Metamath Proof Explorer

Theorem exopxfr

Description: Transfer ordered-pair existence from/to single variable existence. (Contributed by NM, 26-Feb-2014) (Proof shortened by Mario Carneiro, 31-Aug-2015)

Ref Expression
Hypothesis exopxfr.1 ⊢ x = y z → φ ↔ ψ
Assertion exopxfr ⊢ ∃ x ∈ V × V φ ↔ ∃ y ∃ z ψ

Proof

Step Hyp Ref Expression
1 exopxfr.1 ⊢ x = y z → φ ↔ ψ
2 1 rexxp ⊢ ∃ x ∈ V × V φ ↔ ∃ y ∈ V ∃ z ∈ V ψ
3 rexv ⊢ ∃ y ∈ V ∃ z ∈ V ψ ↔ ∃ y ∃ z ∈ V ψ
4 rexv ⊢ ∃ z ∈ V ψ ↔ ∃ z ψ
5 4 exbii ⊢ ∃ y ∃ z ∈ V ψ ↔ ∃ y ∃ z ψ
6 2 3 5 3bitri ⊢ ∃ x ∈ V × V φ ↔ ∃ y ∃ z ψ