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 ⊢ p = a b → ψ ↔ χ
Assertion reu3op ⊢ ∃! p ∈ X × Y ψ ↔ ∃ a ∈ X ∃ b ∈ Y χ ∧ ∃ x ∈ X ∃ y ∈ Y ∀ a ∈ X ∀ b ∈ Y χ → x y = a b

Proof

Step Hyp Ref Expression
1 reu3op.a ⊢ p = a b → ψ ↔ χ
2 reu3 ⊢ ∃! p ∈ X × Y ψ ↔ ∃ p ∈ X × Y ψ ∧ ∃ q ∈ X × Y ∀ p ∈ X × Y ψ → p = q
3 1 rexxp ⊢ ∃ p ∈ X × Y ψ ↔ ∃ a ∈ X ∃ b ∈ Y χ
4 eqeq2 ⊢ q = x y → p = q ↔ p = x y
5 4 imbi2d ⊢ q = x y → ψ → p = q ↔ ψ → p = x y
6 5 ralbidv ⊢ q = x y → ∀ p ∈ X × Y ψ → p = q ↔ ∀ p ∈ X × Y ψ → p = x y
7 6 rexxp ⊢ ∃ q ∈ X × Y ∀ p ∈ X × Y ψ → p = q ↔ ∃ x ∈ X ∃ y ∈ Y ∀ p ∈ X × Y ψ → p = x y
8 eqeq1 ⊢ p = a b → p = x y ↔ a b = x y
9 1 8 imbi12d ⊢ p = a b → ψ → p = x y ↔ χ → a b = x y
10 9 ralxp ⊢ ∀ p ∈ X × Y ψ → p = x y ↔ ∀ a ∈ X ∀ b ∈ Y χ → a b = x y
11 eqcom ⊢ a b = x y ↔ x y = a b
12 11 a1i ⊢ x ∈ X ∧ y ∈ Y ∧ a ∈ X ∧ b ∈ Y → a b = x y ↔ x y = a b
13 12 imbi2d ⊢ x ∈ X ∧ y ∈ Y ∧ a ∈ X ∧ b ∈ Y → χ → a b = x y ↔ χ → x y = a b
14 13 2ralbidva ⊢ x ∈ X ∧ y ∈ Y → ∀ a ∈ X ∀ b ∈ Y χ → a b = x y ↔ ∀ a ∈ X ∀ b ∈ Y χ → x y = a b
15 10 14 bitrid ⊢ x ∈ X ∧ y ∈ Y → ∀ p ∈ X × Y ψ → p = x y ↔ ∀ a ∈ X ∀ b ∈ Y χ → x y = a b
16 15 2rexbiia ⊢ ∃ x ∈ X ∃ y ∈ Y ∀ p ∈ X × Y ψ → p = x y ↔ ∃ x ∈ X ∃ y ∈ Y ∀ a ∈ X ∀ b ∈ Y χ → x y = a b
17 7 16 bitri ⊢ ∃ q ∈ X × Y ∀ p ∈ X × Y ψ → p = q ↔ ∃ x ∈ X ∃ y ∈ Y ∀ a ∈ X ∀ b ∈ Y χ → x y = a b
18 3 17 anbi12i ⊢ ∃ p ∈ X × Y ψ ∧ ∃ q ∈ X × Y ∀ p ∈ X × Y ψ → p = q ↔ ∃ a ∈ X ∃ b ∈ Y χ ∧ ∃ x ∈ X ∃ y ∈ Y ∀ a ∈ X ∀ b ∈ Y χ → x y = a b
19 2 18 bitri ⊢ ∃! p ∈ X × Y ψ ↔ ∃ a ∈ X ∃ b ∈ Y χ ∧ ∃ x ∈ X ∃ y ∈ Y ∀ a ∈ X ∀ b ∈ Y χ → x y = a b