Definition df-wl-rex 34891

Description: Restrict an existential quantifier to a class 𝐴. This version does not interpret elementhood verbatim as ∃𝑥 ∈ 𝐴𝜑 does. Assuming a real elementhood can lead to awkward consequences should the class 𝐴 depend on 𝑥. Instead we base the definition on df-wl-ral 34881, where this is ruled out. Other definitions are wl-dfrexsb 34896 and wl-dfrexex 34895. If 𝑥 is not free in 𝐴, the defining expression can be simplified (see wl-dfrexf 34892, wl-dfrexv 34894).

This definition lets 𝑥 appear as a formal parameter with no connection to 𝐴, but occurrences in 𝜑 are fully honored. (Contributed by NM, 30-Aug-1993.) Isolate x from A. (Revised by Wolf Lammen, 25-May-2023.)

Assertion

Ref	Expression
df-wl-rex	⊢ (∃(𝑥 : 𝐴)𝜑 ↔ ¬ ∀(𝑥 : 𝐴) ¬ 𝜑)

Detailed syntax breakdown of Definition df-wl-rex

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3		cA	. . 3 class 𝐴
4	1, 2, 3	wl-rex 34877	. 2 wff ∃(𝑥 : 𝐴)𝜑
5	1	wn 3	. . . 4 wff ¬ 𝜑
6	5, 2, 3	wl-ral 34876	. . 3 wff ∀(𝑥 : 𝐴) ¬ 𝜑
7	6	wn 3	. 2 wff ¬ ∀(𝑥 : 𝐴) ¬ 𝜑
8	4, 7	wb 208	1 wff (∃(𝑥 : 𝐴)𝜑 ↔ ¬ ∀(𝑥 : 𝐴) ¬ 𝜑)

This definition is referenced by:  wl-dfrexf  34892  wl-dfrexv  34894  wl-dfrexex  34895  wl-dfrexsb  34896