# 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}⟩\to \left({\phi }↔{\chi }\right)$
Assertion 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)$

### Proof

Step Hyp Ref Expression
1 opreu2reurex.a ${⊢}{p}=⟨{a},{b}⟩\to \left({\phi }↔{\chi }\right)$
2 eqcom ${⊢}⟨{x},{y}⟩=⟨{a},{b}⟩↔⟨{a},{b}⟩=⟨{x},{y}⟩$
3 vex ${⊢}{a}\in \mathrm{V}$
4 vex ${⊢}{b}\in \mathrm{V}$
5 3 4 opth ${⊢}⟨{a},{b}⟩=⟨{x},{y}⟩↔\left({a}={x}\wedge {b}={y}\right)$
6 2 5 bitri ${⊢}⟨{x},{y}⟩=⟨{a},{b}⟩↔\left({a}={x}\wedge {b}={y}\right)$
7 6 imbi2i ${⊢}\left({\chi }\to ⟨{x},{y}⟩=⟨{a},{b}⟩\right)↔\left({\chi }\to \left({a}={x}\wedge {b}={y}\right)\right)$
8 7 a1i ${⊢}\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge \left({a}\in {A}\wedge {b}\in {B}\right)\right)\to \left(\left({\chi }\to ⟨{x},{y}⟩=⟨{a},{b}⟩\right)↔\left({\chi }\to \left({a}={x}\wedge {b}={y}\right)\right)\right)$
9 8 2ralbidva ${⊢}\left({x}\in {A}\wedge {y}\in {B}\right)\to \left(\forall {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\left({\chi }\to ⟨{x},{y}⟩=⟨{a},{b}⟩\right)↔\forall {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\left({\chi }\to \left({a}={x}\wedge {b}={y}\right)\right)\right)$
10 9 2rexbiia ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\left({\chi }\to ⟨{x},{y}⟩=⟨{a},{b}⟩\right)↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\left({\chi }\to \left({a}={x}\wedge {b}={y}\right)\right)$
11 10 anbi2i ${⊢}\left(\exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\exists {b}\in {B}\phantom{\rule{.4em}{0ex}}{\chi }\wedge \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\left({\chi }\to ⟨{x},{y}⟩=⟨{a},{b}⟩\right)\right)↔\left(\exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\exists {b}\in {B}\phantom{\rule{.4em}{0ex}}{\chi }\wedge \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\left({\chi }\to \left({a}={x}\wedge {b}={y}\right)\right)\right)$
12 1 reu3op ${⊢}\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 {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\left({\chi }\to ⟨{x},{y}⟩=⟨{a},{b}⟩\right)\right)$
13 2reu4 ${⊢}\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)↔\left(\exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\exists {b}\in {B}\phantom{\rule{.4em}{0ex}}{\chi }\wedge \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\left({\chi }\to \left({a}={x}\wedge {b}={y}\right)\right)\right)$
14 11 12 13 3bitr4i ${⊢}\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)$