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

Metamath Proof Explorer

Theorem opreu2reu

Description: If there is a unique ordered pair fulfilling a wff, then there is a double restricted unique existential qualification fulfilling a corresponding wff. (Contributed by AV, 25-Jun-2023) (Revised by AV, 2-Jul-2023)

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

Proof

Step Hyp Ref Expression
1 opreu2reurex.a ⊢ p = a b → φ ↔ χ
2 1 opreu2reurex ⊢ ∃! p ∈ A × B φ ↔ ∃! a ∈ A ∃ b ∈ B χ ∧ ∃! b ∈ B ∃ a ∈ A χ
3 2rexreu ⊢ ∃! a ∈ A ∃ b ∈ B χ ∧ ∃! b ∈ B ∃ a ∈ A χ → ∃! a ∈ A ∃! b ∈ B χ
4 2 3 sylbi ⊢ ∃! p ∈ A × B φ → ∃! a ∈ A ∃! b ∈ B χ