Theorem: SetTheory.interpret_memPreimage (SetTheory/Relation.lean)

State before:
V : Type u_1
inst✝ : Zermelo V
r✝ x✝ y✝ z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y r : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.memPreimage x y r) v l ↔
    interpretTerm V v l x ∈ preimage (interpretTerm V v l r) (interpretTerm V v l y)
Tactic:
rw [mem_preimage_iff, interpret_memPreimage']
State after:
no goals