Metamath Proof Explorer

Theorem 2sb5

Description: Equivalence for double substitution. (Contributed by NM, 3-Feb-2005)

Ref Expression
Assertion 2sb5 ⊢ z x w y φ ↔ ∃ x ∃ y x = z ∧ y = w ∧ φ

Proof

Step Hyp Ref Expression
1 sb5 ⊢ z x w y φ ↔ ∃ x x = z ∧ w y φ
2 19.42v ⊢ ∃ y x = z ∧ y = w ∧ φ ↔ x = z ∧ ∃ y y = w ∧ φ
3 anass ⊢ x = z ∧ y = w ∧ φ ↔ x = z ∧ y = w ∧ φ
4 3 exbii ⊢ ∃ y x = z ∧ y = w ∧ φ ↔ ∃ y x = z ∧ y = w ∧ φ
5 sb5 ⊢ w y φ ↔ ∃ y y = w ∧ φ
6 5 anbi2i ⊢ x = z ∧ w y φ ↔ x = z ∧ ∃ y y = w ∧ φ
7 2 4 6 3bitr4ri ⊢ x = z ∧ w y φ ↔ ∃ y x = z ∧ y = w ∧ φ
8 7 exbii ⊢ ∃ x x = z ∧ w y φ ↔ ∃ x ∃ y x = z ∧ y = w ∧ φ
9 1 8 bitri ⊢ z x w y φ ↔ ∃ x ∃ y x = z ∧ y = w ∧ φ