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

Theorem abn0 3651
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 2576 . . 3  |-  F/_ x { x  |  ph }
21n0f 3640 . 2  |-  ( { x  |  ph }  =/=  (/)  <->  E. x  x  e. 
{ x  |  ph } )
3 abid 2426 . . 3  |-  ( x  e.  { x  | 
ph }  <->  ph )
43exbii 1634 . 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 1586    e. wcel 1756   {cab 2424    =/= wne 2601   (/)c0 3632
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-v 2969  df-dif 3326  df-nul 3633
This theorem is referenced by:  rabn0  3652  intexab  4445  iinexg  4447  relimasn  5187  mapprc  7210  modom  7505  tz9.1c  7942  scott0  8085  scott0s  8087  cp  8090  karden  8094  acnrcl  8204  aceq3lem  8282  cff  8409  cff1  8419  cfss  8426  domtriomlem  8603  axdclem  8680  nqpr  9175  supmul  10290  hashf1lem2  12201  hashf1  12202  mreiincl  14526  efgval  16205  efger  16206  birthdaylem3  22322  disjex  25885  disjexc  25886  supadd  28371  mblfinlem3  28383  ismblfin  28385  itg2addnc  28399  sdclem1  28592  inisegn0  29349
  Copyright terms: Public domain W3C validator