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

Theorem rexn0 3930
Description: Restricted existential quantification implies its restriction is nonempty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.)
Assertion
Ref Expression
rexn0  |-  ( E. x  e.  A  ph  ->  A  =/=  (/) )
Distinct variable group:    x, A
Allowed substitution hint:    ph( x)

Proof of Theorem rexn0
StepHypRef Expression
1 ne0i 3791 . . 3  |-  ( x  e.  A  ->  A  =/=  (/) )
21a1d 25 . 2  |-  ( x  e.  A  ->  ( ph  ->  A  =/=  (/) ) )
32rexlimiv 2949 1  |-  ( E. x  e.  A  ph  ->  A  =/=  (/) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767    =/= wne 2662   E.wrex 2815   (/)c0 3785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-v 3115  df-dif 3479  df-nul 3786
This theorem is referenced by:  reusv2lem3  4650  reusv7OLD  4659  eusvobj2  6275  isdrs2  15422  ismnd  15730  slwn0  16431  lbsexg  17593  iuncon  19695  grpon0  24880  filbcmb  29834  isbnd2  29882  rencldnfi  30359  stoweidlem14  31314  2reu4  31662  iunconlem2  32815
  Copyright terms: Public domain W3C validator