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	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝜑 ↔ 𝜓 ) )
Assertion	exopxfr	⊢ ( ∃ 𝑥 ∈ ( V × V ) 𝜑 ↔ ∃ 𝑦 ∃ 𝑧 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		exopxfr.1	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝜑 ↔ 𝜓 ) )
2	1	rexxp	⊢ ( ∃ 𝑥 ∈ ( V × V ) 𝜑 ↔ ∃ 𝑦 ∈ V ∃ 𝑧 ∈ V 𝜓 )
3		rexv	⊢ ( ∃ 𝑦 ∈ V ∃ 𝑧 ∈ V 𝜓 ↔ ∃ 𝑦 ∃ 𝑧 ∈ V 𝜓 )
4		rexv	⊢ ( ∃ 𝑧 ∈ V 𝜓 ↔ ∃ 𝑧 𝜓 )
5	4	exbii	⊢ ( ∃ 𝑦 ∃ 𝑧 ∈ V 𝜓 ↔ ∃ 𝑦 ∃ 𝑧 𝜓 )
6	2 3 5	3bitri	⊢ ( ∃ 𝑥 ∈ ( V × V ) 𝜑 ↔ ∃ 𝑦 ∃ 𝑧 𝜓 )