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 \leftrightarrow \chi \right)$$
Assertion	opreu2reu	$$⊢\exists !p\in \left(A\times B\right)\phi \to \exists !a\in A\exists !b\in B\chi$$

Proof

Step	Hyp	Ref	Expression
1		opreu2reurex.a	$$⊢p=⟨a,b⟩\to \left(\phi \leftrightarrow \chi \right)$$
2	1	opreu2reurex	$$⊢\exists !p\in \left(A\times B\right)\phi \leftrightarrow \left(\exists !a\in A\exists b\in B\chi \wedge \exists !b\in B\exists a\in A\chi \right)$$
3		2rexreu	$$⊢\left(\exists !a\in A\exists b\in B\chi \wedge \exists !b\in B\exists a\in A\chi \right)\to \exists !a\in A\exists !b\in B\chi$$
4	2 3	sylbi	$$⊢\exists !p\in \left(A\times B\right)\phi \to \exists !a\in A\exists !b\in B\chi$$