Definition df-wl-rmo

Description: Restrict "at most one" to a given class A . This version does not interpret elementhood verbatim like E* x e. A ph does. Assuming a real elementhood can lead to awkward consequences should the class A depend on x . Instead we base the definition on df-wl-ral , where this is already ruled out.

This definition lets x appear as a formal parameter with no connection to A , but occurrences in ph are fully honored.

Alternate definitions are given in wl-dfrmosb and, if x is not free in A , wl-dfrmov and wl-dfrmof . (Contributed by NM, 30-Aug-1993) Isolate x from A. (Revised by Wolf Lammen, 26-May-2023)

	Ref	Expression
Assertion	df-wl-rmo	$$⊢{\exists }^{*}x:A\phi \leftrightarrow \exists y\forall x:A\left(\phi \to x=y\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		cA	$$classA$$
2		wph	$$wff\phi$$
3	2 0 1	wl-rmo	$$wff{\exists }^{*}x:A\phi$$
4		vy	$$setvary$$
5	0	cv	$$setvarx$$
6	4	cv	$$setvary$$
7	5 6	wceq	$$wffx=y$$
8	2 7	wi	$$wff\left(\phi \to x=y\right)$$
9	8 0 1	wl-ral	$$wff\forall x:A\left(\phi \to x=y\right)$$
10	9 4	wex	$$wff\exists y\forall x:A\left(\phi \to x=y\right)$$
11	3 10	wb	$$wff\left({\exists }^{*}x:A\phi \leftrightarrow \exists y\forall x:A\left(\phi \to x=y\right)\right)$$