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

Metamath Proof Explorer

Theorem reu3op

Description: There is a unique ordered pair fulfilling a wff iff there are uniquely two sets fulfilling a corresponding wff. (Contributed by AV, 1-Jul-2023)

Ref Expression
Hypothesis reu3op.a ⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝜓 ↔ 𝜒 ) )
Assertion reu3op ( ∃! 𝑝 ∈ ( 𝑋 × 𝑌 ) 𝜓 ↔ ( ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑌 𝜒 ∧ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑌 ( 𝜒 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) )

Proof

Step Hyp Ref Expression
1 reu3op.a ⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝜓 ↔ 𝜒 ) )
2 reu3 ⊢ ( ∃! 𝑝 ∈ ( 𝑋 × 𝑌 ) 𝜓 ↔ ( ∃ 𝑝 ∈ ( 𝑋 × 𝑌 ) 𝜓 ∧ ∃ 𝑞 ∈ ( 𝑋 × 𝑌 ) ∀ 𝑝 ∈ ( 𝑋 × 𝑌 ) ( 𝜓 → 𝑝 = 𝑞 ) ) )
3 1 rexxp ⊢ ( ∃ 𝑝 ∈ ( 𝑋 × 𝑌 ) 𝜓 ↔ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑌 𝜒 )
4 eqeq2 ⊢ ( 𝑞 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑝 = 𝑞 ↔ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) )
5 4 imbi2d ⊢ ( 𝑞 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝜓 → 𝑝 = 𝑞 ) ↔ ( 𝜓 → 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
6 5 ralbidv ⊢ ( 𝑞 = ⟨ 𝑥 , 𝑦 ⟩ → ( ∀ 𝑝 ∈ ( 𝑋 × 𝑌 ) ( 𝜓 → 𝑝 = 𝑞 ) ↔ ∀ 𝑝 ∈ ( 𝑋 × 𝑌 ) ( 𝜓 → 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
7 6 rexxp ⊢ ( ∃ 𝑞 ∈ ( 𝑋 × 𝑌 ) ∀ 𝑝 ∈ ( 𝑋 × 𝑌 ) ( 𝜓 → 𝑝 = 𝑞 ) ↔ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 ∀ 𝑝 ∈ ( 𝑋 × 𝑌 ) ( 𝜓 → 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) )
8 eqeq1 ⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
9 1 8 imbi12d ⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 𝜓 → 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( 𝜒 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
10 9 ralxp ⊢ ( ∀ 𝑝 ∈ ( 𝑋 × 𝑌 ) ( 𝜓 → 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑌 ( 𝜒 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
11 eqcom ⊢ ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ )
12 11 a1i ⊢ ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌 ) ) → ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) )
13 12 imbi2d ⊢ ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌 ) ) → ( ( 𝜒 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( 𝜒 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) )
14 13 2ralbidva ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → ( ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑌 ( 𝜒 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑌 ( 𝜒 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) )
15 10 14 bitrid ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → ( ∀ 𝑝 ∈ ( 𝑋 × 𝑌 ) ( 𝜓 → 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑌 ( 𝜒 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) )
16 15 2rexbiia ⊢ ( ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 ∀ 𝑝 ∈ ( 𝑋 × 𝑌 ) ( 𝜓 → 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑌 ( 𝜒 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) )
17 7 16 bitri ⊢ ( ∃ 𝑞 ∈ ( 𝑋 × 𝑌 ) ∀ 𝑝 ∈ ( 𝑋 × 𝑌 ) ( 𝜓 → 𝑝 = 𝑞 ) ↔ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑌 ( 𝜒 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) )
18 3 17 anbi12i ⊢ ( ( ∃ 𝑝 ∈ ( 𝑋 × 𝑌 ) 𝜓 ∧ ∃ 𝑞 ∈ ( 𝑋 × 𝑌 ) ∀ 𝑝 ∈ ( 𝑋 × 𝑌 ) ( 𝜓 → 𝑝 = 𝑞 ) ) ↔ ( ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑌 𝜒 ∧ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑌 ( 𝜒 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) )
19 2 18 bitri ⊢ ( ∃! 𝑝 ∈ ( 𝑋 × 𝑌 ) 𝜓 ↔ ( ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑌 𝜒 ∧ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑌 ( 𝜒 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) )