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

Theorem rexn0 4046
 Description: Restricted existential quantification implies its restriction is nonempty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.)
Assertion
Ref Expression
rexn0 (∃𝑥𝐴 𝜑𝐴 ≠ ∅)
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rexn0
StepHypRef Expression
1 ne0i 3897 . . 3 (𝑥𝐴𝐴 ≠ ∅)
21a1d 25 . 2 (𝑥𝐴 → (𝜑𝐴 ≠ ∅))
32rexlimiv 3020 1 (∃𝑥𝐴 𝜑𝐴 ≠ ∅)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 1987   ≠ wne 2790  ∃wrex 2908  ∅c0 3891 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-v 3188  df-dif 3558  df-nul 3892 This theorem is referenced by:  reusv2lem3  4831  eusvobj2  6597  isdrs2  16860  ismnd  17218  slwn0  17951  lbsexg  19083  iunconn  21141  grpon0  27202  filbcmb  33164  isbnd2  33211  rencldnfi  36862  iunconnlem2  38651  stoweidlem14  39535  hoidmvval0  40105  2reu4  40491
 Copyright terms: Public domain W3C validator