Mathbox for Wolf Lammen < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-wl-rex Structured version   Visualization version   GIF version

Definition df-wl-rex 35027
 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 35017, where this is ruled out. Other definitions are wl-dfrexsb 35032 and wl-dfrexex 35031. If 𝑥 is not free in 𝐴, the defining expression can be simplified (see wl-dfrexf 35028, wl-dfrexv 35030). 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
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
3 cA . . 3 class 𝐴
41, 2, 3wl-rex 35013 . 2 wff ∃(𝑥 : 𝐴)𝜑
51wn 3 . . . 4 wff ¬ 𝜑
65, 2, 3wl-ral 35012 . . 3 wff ∀(𝑥 : 𝐴) ¬ 𝜑
76wn 3 . 2 wff ¬ ∀(𝑥 : 𝐴) ¬ 𝜑
84, 7wb 209 1 wff (∃(𝑥 : 𝐴)𝜑 ↔ ¬ ∀(𝑥 : 𝐴) ¬ 𝜑)
 Colors of variables: wff setvar class This definition is referenced by:  wl-dfrexf  35028  wl-dfrexv  35030  wl-dfrexex  35031  wl-dfrexsb  35032
 Copyright terms: Public domain W3C validator