Theorem euop2

Description: Transfer existential uniqueness to second member of an ordered pair. (Contributed by NM, 10-Apr-2004)

	Ref	Expression
Hypothesis	euop2.1	$$⊢A\in \mathrm{V}$$
Assertion	euop2	$$⊢\exists !x\exists y\left(x=⟨A,y⟩\wedge \phi \right)\leftrightarrow \exists !y\phi$$

Proof

Step	Hyp	Ref	Expression
1		euop2.1	$$⊢A\in \mathrm{V}$$
2		opex	$$⊢⟨A,y⟩\in \mathrm{V}$$
3	1	moop2	$$⊢{\exists }^{*}yx=⟨A,y⟩$$
4	2 3	euxfr2w	$$⊢\exists !x\exists y\left(x=⟨A,y⟩\wedge \phi \right)\leftrightarrow \exists !y\phi$$