Theorem opreu2reu1

Description: Equivalent definition of the double restricted existential uniqueness quantifier, using uniqueness of ordered pairs. (Contributed by Thierry Arnoux, 4-Jul-2023)

	Ref	Expression
Hypothesis	opreu2reu1.a	$$⊢p=⟨x,y⟩\to \left(\chi \leftrightarrow \phi \right)$$
Assertion	opreu2reu1	$$⊢\exists !x\in A,y\in B\phi \leftrightarrow \exists !p\in \left(A\times B\right)\chi$$

Proof

Step	Hyp	Ref	Expression
1		opreu2reu1.a	$$⊢p=⟨x,y⟩\to \left(\chi \leftrightarrow \phi \right)$$
2		df-2reu	$$⊢\exists !x\in A,y\in B\phi \leftrightarrow \left(\exists !x\in A\exists y\in B\phi \wedge \exists !y\in B\exists x\in A\phi \right)$$
3	1	opreu2reurex	$$⊢\exists !p\in \left(A\times B\right)\chi \leftrightarrow \left(\exists !x\in A\exists y\in B\phi \wedge \exists !y\in B\exists x\in A\phi \right)$$
4	2 3	bitr4i	$$⊢\exists !x\in A,y\in B\phi \leftrightarrow \exists !p\in \left(A\times B\right)\chi$$