# Metamath Proof Explorer

## Theorem opreuopreu

Description: There is a unique ordered pair fulfilling a wff iff its components fulfil a corresponding wff. (Contributed by AV, 2-Jul-2023)

Ref Expression
Hypothesis opreuopreu.a ${⊢}\left({a}={1}^{st}\left({p}\right)\wedge {b}={2}^{nd}\left({p}\right)\right)\to \left({\psi }↔{\phi }\right)$
Assertion opreuopreu ${⊢}\exists !{p}\in \left({A}×{B}\right)\phantom{\rule{.4em}{0ex}}{\phi }↔\exists !{p}\in \left({A}×{B}\right)\phantom{\rule{.4em}{0ex}}\exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({p}=⟨{a},{b}⟩\wedge {\psi }\right)$

### Proof

Step Hyp Ref Expression
1 opreuopreu.a ${⊢}\left({a}={1}^{st}\left({p}\right)\wedge {b}={2}^{nd}\left({p}\right)\right)\to \left({\psi }↔{\phi }\right)$
2 elxpi ${⊢}{p}\in \left({A}×{B}\right)\to \exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({p}=⟨{a},{b}⟩\wedge \left({a}\in {A}\wedge {b}\in {B}\right)\right)$
3 simprl ${⊢}\left({\phi }\wedge \left({p}=⟨{a},{b}⟩\wedge \left({a}\in {A}\wedge {b}\in {B}\right)\right)\right)\to {p}=⟨{a},{b}⟩$
4 vex ${⊢}{a}\in \mathrm{V}$
5 vex ${⊢}{b}\in \mathrm{V}$
6 4 5 op1st ${⊢}{1}^{st}\left(⟨{a},{b}⟩\right)={a}$
7 6 eqcomi ${⊢}{a}={1}^{st}\left(⟨{a},{b}⟩\right)$
8 4 5 op2nd ${⊢}{2}^{nd}\left(⟨{a},{b}⟩\right)={b}$
9 8 eqcomi ${⊢}{b}={2}^{nd}\left(⟨{a},{b}⟩\right)$
10 7 9 pm3.2i ${⊢}\left({a}={1}^{st}\left(⟨{a},{b}⟩\right)\wedge {b}={2}^{nd}\left(⟨{a},{b}⟩\right)\right)$
11 fveq2 ${⊢}{p}=⟨{a},{b}⟩\to {1}^{st}\left({p}\right)={1}^{st}\left(⟨{a},{b}⟩\right)$
12 11 eqeq2d ${⊢}{p}=⟨{a},{b}⟩\to \left({a}={1}^{st}\left({p}\right)↔{a}={1}^{st}\left(⟨{a},{b}⟩\right)\right)$
13 fveq2 ${⊢}{p}=⟨{a},{b}⟩\to {2}^{nd}\left({p}\right)={2}^{nd}\left(⟨{a},{b}⟩\right)$
14 13 eqeq2d ${⊢}{p}=⟨{a},{b}⟩\to \left({b}={2}^{nd}\left({p}\right)↔{b}={2}^{nd}\left(⟨{a},{b}⟩\right)\right)$
15 12 14 anbi12d ${⊢}{p}=⟨{a},{b}⟩\to \left(\left({a}={1}^{st}\left({p}\right)\wedge {b}={2}^{nd}\left({p}\right)\right)↔\left({a}={1}^{st}\left(⟨{a},{b}⟩\right)\wedge {b}={2}^{nd}\left(⟨{a},{b}⟩\right)\right)\right)$
16 10 15 mpbiri ${⊢}{p}=⟨{a},{b}⟩\to \left({a}={1}^{st}\left({p}\right)\wedge {b}={2}^{nd}\left({p}\right)\right)$
17 16 1 syl ${⊢}{p}=⟨{a},{b}⟩\to \left({\psi }↔{\phi }\right)$
18 17 biimprd ${⊢}{p}=⟨{a},{b}⟩\to \left({\phi }\to {\psi }\right)$
19 18 adantr ${⊢}\left({p}=⟨{a},{b}⟩\wedge \left({a}\in {A}\wedge {b}\in {B}\right)\right)\to \left({\phi }\to {\psi }\right)$
20 19 impcom ${⊢}\left({\phi }\wedge \left({p}=⟨{a},{b}⟩\wedge \left({a}\in {A}\wedge {b}\in {B}\right)\right)\right)\to {\psi }$
21 3 20 jca ${⊢}\left({\phi }\wedge \left({p}=⟨{a},{b}⟩\wedge \left({a}\in {A}\wedge {b}\in {B}\right)\right)\right)\to \left({p}=⟨{a},{b}⟩\wedge {\psi }\right)$
22 21 ex ${⊢}{\phi }\to \left(\left({p}=⟨{a},{b}⟩\wedge \left({a}\in {A}\wedge {b}\in {B}\right)\right)\to \left({p}=⟨{a},{b}⟩\wedge {\psi }\right)\right)$
23 22 2eximdv ${⊢}{\phi }\to \left(\exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({p}=⟨{a},{b}⟩\wedge \left({a}\in {A}\wedge {b}\in {B}\right)\right)\to \exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({p}=⟨{a},{b}⟩\wedge {\psi }\right)\right)$
24 2 23 syl5com ${⊢}{p}\in \left({A}×{B}\right)\to \left({\phi }\to \exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({p}=⟨{a},{b}⟩\wedge {\psi }\right)\right)$
25 17 biimpa ${⊢}\left({p}=⟨{a},{b}⟩\wedge {\psi }\right)\to {\phi }$
26 25 a1i ${⊢}{p}\in \left({A}×{B}\right)\to \left(\left({p}=⟨{a},{b}⟩\wedge {\psi }\right)\to {\phi }\right)$
27 26 exlimdvv ${⊢}{p}\in \left({A}×{B}\right)\to \left(\exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({p}=⟨{a},{b}⟩\wedge {\psi }\right)\to {\phi }\right)$
28 24 27 impbid ${⊢}{p}\in \left({A}×{B}\right)\to \left({\phi }↔\exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({p}=⟨{a},{b}⟩\wedge {\psi }\right)\right)$
29 28 reubiia ${⊢}\exists !{p}\in \left({A}×{B}\right)\phantom{\rule{.4em}{0ex}}{\phi }↔\exists !{p}\in \left({A}×{B}\right)\phantom{\rule{.4em}{0ex}}\exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({p}=⟨{a},{b}⟩\wedge {\psi }\right)$