Definition df-wl-rex

Description: Restrict an existential quantifier to a class A . This version does not interpret elementhood verbatim as 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. Other definitions are wl-dfrexsb and wl-dfrexex . If x is not free in A , the defining expression can be simplified (see wl-dfrexf , wl-dfrexv ).

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

	Ref	Expression
Assertion	df-wl-rex	$$⊢\exists x:A\phi \leftrightarrow \neg \forall x:A\neg \phi$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		cA	$$classA$$
2		wph	$$wff\phi$$
3	2 0 1	wl-rex	$$wff\exists x:A\phi$$
4	2	wn	$$wff\neg \phi$$
5	4 0 1	wl-ral	$$wff\forall x:A\neg \phi$$
6	5	wn	$$wff\neg \forall x:A\neg \phi$$
7	3 6	wb	$$wff\left(\exists x:A\phi \leftrightarrow \neg \forall x:A\neg \phi \right)$$