rw [mem_id_iff, interpret_memId']
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.memId x y) v l ↔ interpretTerm V v l x ∈ id (interpretTerm V v l y)
no goals