This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐴 → ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑦 ∃ 𝑧 ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐴 ∧ 𝜓 ) ) )