Theorem exopxfr2

Description: Transfer ordered-pair existence from/to single variable existence. (Contributed by NM, 26-Feb-2014)

	Ref	Expression
Hypothesis	exopxfr2.1	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝜑 ↔ 𝜓 ) )
Assertion	exopxfr2	⊢ ( Rel 𝐴 → ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑦 ∃ 𝑧 ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐴 ∧ 𝜓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		exopxfr2.1	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝜑 ↔ 𝜓 ) )
2		df-rel	⊢ ( Rel 𝐴 ↔ 𝐴 ⊆ ( V × V ) )
3	2	biimpi	⊢ ( Rel 𝐴 → 𝐴 ⊆ ( V × V ) )
4	3	sseld	⊢ ( Rel 𝐴 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( V × V ) ) )
5	4	adantrd	⊢ ( Rel 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → 𝑥 ∈ ( V × V ) ) )
6	5	pm4.71rd	⊢ ( Rel 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝑥 ∈ ( V × V ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ) )
7	6	rexbidv2	⊢ ( Rel 𝐴 → ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ∈ ( V × V ) ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
8		eleq1	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝑥 ∈ 𝐴 ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐴 ) )
9	8 1	anbi12d	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐴 ∧ 𝜓 ) ) )
10	9	exopxfr	⊢ ( ∃ 𝑥 ∈ ( V × V ) ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ∃ 𝑦 ∃ 𝑧 ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐴 ∧ 𝜓 ) )
11	7 10	bitrdi	⊢ ( Rel 𝐴 → ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑦 ∃ 𝑧 ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐴 ∧ 𝜓 ) ) )