Theorem rmo2

Description: Alternate definition of restricted "at most one." Note that E* x e. A ph is not equivalent to E. y e. A A. x e. A ( ph -> x = y ) (in analogy to reu6 ); to see this, let A be the empty set. However, one direction of this pattern holds; see rmo2i . (Contributed by NM, 17-Jun-2017)

	Ref	Expression
Hypothesis	rmo2.1	$$⊢Ⅎy\phi$$
Assertion	rmo2	$$⊢{\exists }^{*}x\in A\phi \leftrightarrow \exists y\forall x\in A\left(\phi \to x=y\right)$$

Proof

Step	Hyp	Ref	Expression
1		rmo2.1	$$⊢Ⅎy\phi$$
2		df-rmo	$$⊢{\exists }^{*}x\in A\phi \leftrightarrow {\exists }^{*}x\left(x\in A\wedge \phi \right)$$
3		nfv	$$⊢Ⅎyx\in A$$
4	3 1	nfan	$$⊢Ⅎy\left(x\in A\wedge \phi \right)$$
5	4	mof	$$⊢{\exists }^{*}x\left(x\in A\wedge \phi \right)\leftrightarrow \exists y\forall x\left(\left(x\in A\wedge \phi \right)\to x=y\right)$$
6		impexp	$$⊢\left(\left(x\in A\wedge \phi \right)\to x=y\right)\leftrightarrow \left(x\in A\to \left(\phi \to x=y\right)\right)$$
7	6	albii	$$⊢\forall x\left(\left(x\in A\wedge \phi \right)\to x=y\right)\leftrightarrow \forall x\left(x\in A\to \left(\phi \to x=y\right)\right)$$
8		df-ral	$$⊢\forall x\in A\left(\phi \to x=y\right)\leftrightarrow \forall x\left(x\in A\to \left(\phi \to x=y\right)\right)$$
9	7 8	bitr4i	$$⊢\forall x\left(\left(x\in A\wedge \phi \right)\to x=y\right)\leftrightarrow \forall x\in A\left(\phi \to x=y\right)$$
10	9	exbii	$$⊢\exists y\forall x\left(\left(x\in A\wedge \phi \right)\to x=y\right)\leftrightarrow \exists y\forall x\in A\left(\phi \to x=y\right)$$
11	2 5 10	3bitri	$$⊢{\exists }^{*}x\in A\phi \leftrightarrow \exists y\forall x\in A\left(\phi \to x=y\right)$$