Definition df-wl-reu

Description: Restrict existential uniqueness 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 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-dfreusb and, if x is not free in A , wl-dfreuv and wl-dfreuf . (Contributed by NM, 30-Aug-1993) Isolate x from A. (Revised by Wolf Lammen, 28-May-2023)

	Ref	Expression
Assertion	df-wl-reu	$$⊢\exists !x:A\phi \leftrightarrow \left(\exists x:A\phi \wedge {\exists }^{*}x:A\phi \right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		cA	$$classA$$
2		wph	$$wff\phi$$
3	2 0 1	wl-reu	$$wff\exists !x:A\phi$$
4	2 0 1	wl-rex	$$wff\exists x:A\phi$$
5	2 0 1	wl-rmo	$$wff{\exists }^{*}x:A\phi$$
6	4 5	wa	$$wff\left(\exists x:A\phi \wedge {\exists }^{*}x:A\phi \right)$$
7	3 6	wb	$$wff\left(\exists !x:A\phi \leftrightarrow \left(\exists x:A\phi \wedge {\exists }^{*}x:A\phi \right)\right)$$