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

Metamath Proof Explorer

Theorem opreu2reurex

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

Ref Expression
Hypothesis opreu2reurex.a ⊢ p = a b → φ ↔ χ
Assertion opreu2reurex ⊢ ∃! p ∈ A × B φ ↔ ∃! a ∈ A ∃ b ∈ B χ ∧ ∃! b ∈ B ∃ a ∈ A χ

Proof

Step Hyp Ref Expression
1 opreu2reurex.a ⊢ p = a b → φ ↔ χ
2 eqcom ⊢ x y = a b ↔ a b = x y
3 vex ⊢ a ∈ V
4 vex ⊢ b ∈ V
5 3 4 opth ⊢ a b = x y ↔ a = x ∧ b = y
6 2 5 bitri ⊢ x y = a b ↔ a = x ∧ b = y
7 6 imbi2i ⊢ χ → x y = a b ↔ χ → a = x ∧ b = y
8 7 a1i ⊢ x ∈ A ∧ y ∈ B ∧ a ∈ A ∧ b ∈ B → χ → x y = a b ↔ χ → a = x ∧ b = y
9 8 2ralbidva ⊢ x ∈ A ∧ y ∈ B → ∀ a ∈ A ∀ b ∈ B χ → x y = a b ↔ ∀ a ∈ A ∀ b ∈ B χ → a = x ∧ b = y
10 9 2rexbiia ⊢ ∃ x ∈ A ∃ y ∈ B ∀ a ∈ A ∀ b ∈ B χ → x y = a b ↔ ∃ x ∈ A ∃ y ∈ B ∀ a ∈ A ∀ b ∈ B χ → a = x ∧ b = y
11 10 anbi2i ⊢ ∃ a ∈ A ∃ b ∈ B χ ∧ ∃ x ∈ A ∃ y ∈ B ∀ a ∈ A ∀ b ∈ B χ → x y = a b ↔ ∃ a ∈ A ∃ b ∈ B χ ∧ ∃ x ∈ A ∃ y ∈ B ∀ a ∈ A ∀ b ∈ B χ → a = x ∧ b = y
12 1 reu3op ⊢ ∃! p ∈ A × B φ ↔ ∃ a ∈ A ∃ b ∈ B χ ∧ ∃ x ∈ A ∃ y ∈ B ∀ a ∈ A ∀ b ∈ B χ → x y = a b
13 2reu4 ⊢ ∃! a ∈ A ∃ b ∈ B χ ∧ ∃! b ∈ B ∃ a ∈ A χ ↔ ∃ a ∈ A ∃ b ∈ B χ ∧ ∃ x ∈ A ∃ y ∈ B ∀ a ∈ A ∀ b ∈ B χ → a = x ∧ b = y
14 11 12 13 3bitr4i ⊢ ∃! p ∈ A × B φ ↔ ∃! a ∈ A ∃ b ∈ B χ ∧ ∃! b ∈ B ∃ a ∈ A χ