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

Theorem abn0 3589
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 2525 . . 3  |-  F/_ x { x  |  ph }
21n0f 3579 . 2  |-  ( { x  |  ph }  =/=  (/)  <->  E. x  x  e. 
{ x  |  ph } )
3 abid 2375 . . 3  |-  ( x  e.  { x  | 
ph }  <->  ph )
43exbii 1589 . 2  |-  ( E. x  x  e.  {
x  |  ph }  <->  E. x ph )
52, 4bitri 241 1  |-  ( { x  |  ph }  =/=  (/)  <->  E. x ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 177   E.wex 1547    e. wcel 1717   {cab 2373    =/= wne 2550   (/)c0 3571
This theorem is referenced by:  rabn0  3590  intexab  4299  iinexg  4301  relimasn  5167  mapprc  6958  modom  7245  tz9.1c  7599  scott0  7743  scott0s  7745  cp  7748  karden  7752  acnrcl  7856  aceq3lem  7934  cff  8061  cff1  8071  cfss  8078  domtriomlem  8255  axdclem  8332  nqpr  8824  supmul  9908  hashf1lem2  11632  hashf1  11633  mreiincl  13748  efgval  15276  efger  15277  birthdaylem3  20659  disjex  23875  disjexc  23876  supadd  25948  itg2addnc  25959  sdclem1  26138  inisegn0  26809
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-v 2901  df-dif 3266  df-nul 3572
  Copyright terms: Public domain W3C validator