Definition df-wl-reu 34855

Description: Restrict existential uniqueness to a given class 𝐴. This version does not interpret elementhood verbatim like ∃!𝑥 ∈ 𝐴𝜑 does. Assuming a real elementhood can lead to awkward consequences should the class 𝐴 depend on 𝑥. Instead we base the definition on df-wl-ral 34835, where this is ruled out.

This definition lets 𝑥 appear as a formal parameter with no connection to 𝐴, but occurrences in 𝜑 are fully honored.

Alternate definitions are given in wl-dfreusb 34856 and, if 𝑥 is not free in 𝐴, wl-dfreuv 34857 and wl-dfreuf 34858. (Contributed by NM, 30-Aug-1993.) Isolate x from A. (Revised by Wolf Lammen, 28-May-2023.)

Assertion

Ref	Expression
df-wl-reu	⊢ (∃!(𝑥 : 𝐴)𝜑 ↔ (∃(𝑥 : 𝐴)𝜑 ∧ ∃*(𝑥 : 𝐴)𝜑))

Detailed syntax breakdown of Definition df-wl-reu

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3		cA	. . 3 class 𝐴
4	1, 2, 3	wl-reu 34833	. 2 wff ∃!(𝑥 : 𝐴)𝜑
5	1, 2, 3	wl-rex 34831	. . 3 wff ∃(𝑥 : 𝐴)𝜑
6	1, 2, 3	wl-rmo 34832	. . 3 wff ∃*(𝑥 : 𝐴)𝜑
7	5, 6	wa 398	. 2 wff (∃(𝑥 : 𝐴)𝜑 ∧ ∃*(𝑥 : 𝐴)𝜑)
8	4, 7	wb 208	1 wff (∃!(𝑥 : 𝐴)𝜑 ↔ (∃(𝑥 : 𝐴)𝜑 ∧ ∃*(𝑥 : 𝐴)𝜑))

This definition is referenced by:  wl-dfreusb  34856  wl-dfreuv  34857  wl-dfreuf  34858