Theorem reu4

Description: Restricted uniqueness using implicit substitution. (Contributed by NM, 23-Nov-1994)

	Ref	Expression
Hypothesis	rmo4.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	reu4	$$⊢\exists !x\in A\phi \leftrightarrow \left(\exists x\in A\phi \wedge \forall x\in A\forall y\in A\left(\left(\phi \wedge \psi \right)\to x=y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		rmo4.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
2		reu5	$$⊢\exists !x\in A\phi \leftrightarrow \left(\exists x\in A\phi \wedge {\exists }^{*}x\in A\phi \right)$$
3	1	rmo4	$$⊢{\exists }^{*}x\in A\phi \leftrightarrow \forall x\in A\forall y\in A\left(\left(\phi \wedge \psi \right)\to x=y\right)$$
4	3	anbi2i	$$⊢\left(\exists x\in A\phi \wedge {\exists }^{*}x\in A\phi \right)\leftrightarrow \left(\exists x\in A\phi \wedge \forall x\in A\forall y\in A\left(\left(\phi \wedge \psi \right)\to x=y\right)\right)$$
5	2 4	bitri	$$⊢\exists !x\in A\phi \leftrightarrow \left(\exists x\in A\phi \wedge \forall x\in A\forall y\in A\left(\left(\phi \wedge \psi \right)\to x=y\right)\right)$$