MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexn0 Structured version   Visualization version   GIF version

Theorem rexn0 4505
Description: Restricted existential quantification implies its restriction is nonempty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) Avoid df-clel 2803, ax-8 2101. (Revised by GG, 2-Sep-2024.)
Assertion
Ref Expression
rexn0 (∃𝑥𝐴 𝜑𝐴 ≠ ∅)
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rexn0
StepHypRef Expression
1 dfrex2 3063 . . 3 (∃𝑥𝐴 𝜑 ↔ ¬ ∀𝑥𝐴 ¬ 𝜑)
2 rzal 4503 . . . 4 (𝐴 = ∅ → ∀𝑥𝐴 ¬ 𝜑)
32con3i 154 . . 3 (¬ ∀𝑥𝐴 ¬ 𝜑 → ¬ 𝐴 = ∅)
41, 3sylbi 216 . 2 (∃𝑥𝐴 𝜑 → ¬ 𝐴 = ∅)
54neqned 2937 1 (∃𝑥𝐴 𝜑𝐴 ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1534  wne 2930  wral 3051  wrex 3060  c0 4322
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-ne 2931  df-ral 3052  df-rex 3061  df-dif 3949  df-nul 4323
This theorem is referenced by:  2reu4  4521  reusv2lem3  5396  eusvobj2  7408  isdrs2  18326  ismnd  18725  slwn0  19609  lbsexg  21141  iunconn  23420  sltn0  27925  grpon0  30432  filbcmb  37454  isbnd2  37497  rencldnfi  42515  iunconnlem2  44648  stoweidlem14  45671  hoidmvval0  46244  thinciso  48417
  Copyright terms: Public domain W3C validator