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

Theorem abn0 3790
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 2607 . . 3  |-  F/_ x { x  |  ph }
21n0f 3779 . 2  |-  ( { x  |  ph }  =/=  (/)  <->  E. x  x  e. 
{ x  |  ph } )
3 abid 2430 . . 3  |-  ( x  e.  { x  | 
ph }  <->  ph )
43exbii 1654 . 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 1599    e. wcel 1804   {cab 2428    =/= wne 2638   (/)c0 3770
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-v 3097  df-dif 3464  df-nul 3771
This theorem is referenced by:  rabn0  3791  intexab  4595  iinexg  4597  relimasn  5350  mapprc  7426  modom  7722  tz9.1c  8164  scott0  8307  scott0s  8309  cp  8312  karden  8316  acnrcl  8426  aceq3lem  8504  cff  8631  cff1  8641  cfss  8648  domtriomlem  8825  axdclem  8902  nqpr  9395  supmul  10517  hashf1lem2  12484  hashf1  12485  mreiincl  14870  efgval  16609  efger  16610  birthdaylem3  23155  disjex  27323  disjexc  27324  mppsval  28805  supadd  30017  mblfinlem3  30028  ismblfin  30030  itg2addnc  30044  sdclem1  30211  inisegn0  30964  upbdrech  31454
  Copyright terms: Public domain W3C validator