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

Theorem wl-dfrexf 35011
Description: Restricted existential quantification (df-wl-rex 35010) allows a simplification, if we can assume all occurrences of 𝑥 in 𝐴 are bounded. (Contributed by Wolf Lammen, 25-May-2023.)
Assertion
Ref Expression
wl-dfrexf (𝑥𝐴 → (∃(𝑥 : 𝐴)𝜑 ↔ ∃𝑥(𝑥𝐴𝜑)))

Proof of Theorem wl-dfrexf
StepHypRef Expression
1 wl-dfralf 35003 . . 3 (𝑥𝐴 → (∀(𝑥 : 𝐴) ¬ 𝜑 ↔ ∀𝑥(𝑥𝐴 → ¬ 𝜑)))
21notbid 321 . 2 (𝑥𝐴 → (¬ ∀(𝑥 : 𝐴) ¬ 𝜑 ↔ ¬ ∀𝑥(𝑥𝐴 → ¬ 𝜑)))
3 df-wl-rex 35010 . 2 (∃(𝑥 : 𝐴)𝜑 ↔ ¬ ∀(𝑥 : 𝐴) ¬ 𝜑)
4 exnalimn 1845 . 2 (∃𝑥(𝑥𝐴𝜑) ↔ ¬ ∀𝑥(𝑥𝐴 → ¬ 𝜑))
52, 3, 43bitr4g 317 1 (𝑥𝐴 → (∃(𝑥 : 𝐴)𝜑 ↔ ∃𝑥(𝑥𝐴𝜑)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wal 1536  wex 1781  wcel 2112  wnfc 2939  wl-ral 34995  wl-rex 34996
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-11 2159  ax-12 2176
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-clel 2873  df-nfc 2941  df-wl-ral 35000  df-wl-rex 35010
This theorem is referenced by:  wl-dfrexfi  35012  wl-dfreuf  35023
  Copyright terms: Public domain W3C validator