rw [mem_rcomp_iff, interpret_memRComp']
V : Type u_1
inst✝ : Zermelo V
r✝ x✝ y z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x s r : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.memRComp x s r) v l ↔
    interpretTerm V v l x ∈ rcomp (interpretTerm V v l s) (interpretTerm V v l r)
no goals