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

Theorem abn0 3486
Description: Nonempty class abstraction. (Contributed by NM, 26-Dec-1996.) (Proof shortened by Mario Carneiro, 11-Nov-2016.)
Assertion
Ref Expression
abn0  |-  ( { x  |  ph }  =/=  (/)  <->  E. x ph )

Proof of Theorem abn0
StepHypRef Expression
1 nfab1 2434 . . 3  |-  F/_ x { x  |  ph }
21n0f 3476 . 2  |-  ( { x  |  ph }  =/=  (/)  <->  E. x  x  e. 
{ x  |  ph } )
3 abid 2284 . . 3  |-  ( x  e.  { x  | 
ph }  <->  ph )
43exbii 1572 . 2  |-  ( E. x  x  e.  {
x  |  ph }  <->  E. x ph )
52, 4bitri 240 1  |-  ( { x  |  ph }  =/=  (/)  <->  E. x ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 176   E.wex 1531    e. wcel 1696   {cab 2282    =/= wne 2459   (/)c0 3468
This theorem is referenced by:  rabn0  3487  intexab  4185  iinexg  4187  relimasn  5052  mapprc  6792  modom  7079  tz9.1c  7428  scott0  7572  scott0s  7574  cp  7577  karden  7581  acnrcl  7685  aceq3lem  7763  cff  7890  cff1  7900  cfss  7907  domtriomlem  8084  axdclem  8162  nqpr  8654  supmul  9738  hashf1lem2  11410  hashf1  11411  mreiincl  13514  efgval  15042  efger  15043  birthdaylem3  20264  disjex  23192  disjexc  23193  supadd  24996  itg2addnc  25005  indcls2  26099  sdclem1  26556  inisegn0  27243
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-v 2803  df-dif 3168  df-nul 3469
  Copyright terms: Public domain W3C validator