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

Theorem abn0 3809
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 2631 . . 3  |-  F/_ x { x  |  ph }
21n0f 3798 . 2  |-  ( { x  |  ph }  =/=  (/)  <->  E. x  x  e. 
{ x  |  ph } )
3 abid 2454 . . 3  |-  ( x  e.  { x  | 
ph }  <->  ph )
43exbii 1644 . 2  |-  ( E. x  x  e.  {
x  |  ph }  <->  E. x ph )
52, 4bitri 249 1  |-  ( { x  |  ph }  =/=  (/)  <->  E. x ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   E.wex 1596    e. wcel 1767   {cab 2452    =/= wne 2662   (/)c0 3790
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-or 370  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-v 3120  df-dif 3484  df-nul 3791
This theorem is referenced by:  rabn0  3810  intexab  4611  iinexg  4613  relimasn  5366  mapprc  7436  modom  7732  tz9.1c  8173  scott0  8316  scott0s  8318  cp  8321  karden  8325  acnrcl  8435  aceq3lem  8513  cff  8640  cff1  8650  cfss  8657  domtriomlem  8834  axdclem  8911  nqpr  9404  supmul  10523  hashf1lem2  12486  hashf1  12487  mreiincl  14868  efgval  16608  efger  16609  birthdaylem3  23149  disjex  27265  disjexc  27266  mppsval  28748  supadd  29960  mblfinlem3  29971  ismblfin  29973  itg2addnc  29987  sdclem1  30154  inisegn0  30908  upbdrech  31396
  Copyright terms: Public domain W3C validator