# 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}⟩\to \left({\phi }↔{\chi }\right)$
Assertion opreu2reu ${⊢}\exists !{p}\in \left({A}×{B}\right)\phantom{\rule{.4em}{0ex}}{\phi }\to \exists !{a}\in {A}\phantom{\rule{.4em}{0ex}}\exists !{b}\in {B}\phantom{\rule{.4em}{0ex}}{\chi }$

### Proof

Step Hyp Ref Expression
1 opreu2reurex.a ${⊢}{p}=⟨{a},{b}⟩\to \left({\phi }↔{\chi }\right)$
2 1 opreu2reurex ${⊢}\exists !{p}\in \left({A}×{B}\right)\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\exists !{a}\in {A}\phantom{\rule{.4em}{0ex}}\exists {b}\in {B}\phantom{\rule{.4em}{0ex}}{\chi }\wedge \exists !{b}\in {B}\phantom{\rule{.4em}{0ex}}\exists {a}\in {A}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
3 2rexreu ${⊢}\left(\exists !{a}\in {A}\phantom{\rule{.4em}{0ex}}\exists {b}\in {B}\phantom{\rule{.4em}{0ex}}{\chi }\wedge \exists !{b}\in {B}\phantom{\rule{.4em}{0ex}}\exists {a}\in {A}\phantom{\rule{.4em}{0ex}}{\chi }\right)\to \exists !{a}\in {A}\phantom{\rule{.4em}{0ex}}\exists !{b}\in {B}\phantom{\rule{.4em}{0ex}}{\chi }$
4 2 3 sylbi ${⊢}\exists !{p}\in \left({A}×{B}\right)\phantom{\rule{.4em}{0ex}}{\phi }\to \exists !{a}\in {A}\phantom{\rule{.4em}{0ex}}\exists !{b}\in {B}\phantom{\rule{.4em}{0ex}}{\chi }$