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

Theorem abn0 3473
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 2421 . . 3  |-  F/_ x { x  |  ph }
21n0f 3463 . 2  |-  ( { x  |  ph }  =/=  (/)  <->  E. x  x  e. 
{ x  |  ph } )
3 abid 2271 . . 3  |-  ( x  e.  { x  | 
ph }  <->  ph )
43exbii 1569 . 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 1528    e. wcel 1684   {cab 2269    =/= wne 2446   (/)c0 3455
This theorem is referenced by:  rabn0  3474  intexab  4169  iinexg  4171  relimasn  5036  mapprc  6776  modom  7063  tz9.1c  7412  scott0  7556  scott0s  7558  cp  7561  karden  7565  acnrcl  7669  aceq3lem  7747  cff  7874  cff1  7884  cfss  7891  domtriomlem  8068  axdclem  8146  nqpr  8638  supmul  9722  hashf1lem2  11394  hashf1  11395  mreiincl  13498  efgval  15026  efger  15027  birthdaylem3  20248  disjex  23176  disjexc  23177  indcls2  25996  sdclem1  26453  inisegn0  27140
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-v 2790  df-dif 3155  df-nul 3456
  Copyright terms: Public domain W3C validator