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

Theorem abn0 3638
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 2573 . . 3  |-  F/_ x { x  |  ph }
21n0f 3628 . 2  |-  ( { x  |  ph }  =/=  (/)  <->  E. x  x  e. 
{ x  |  ph } )
3 abid 2423 . . 3  |-  ( x  e.  { x  | 
ph }  <->  ph )
43exbii 1592 . 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 1550    e. wcel 1725   {cab 2421    =/= wne 2598   (/)c0 3620
This theorem is referenced by:  rabn0  3639  intexab  4350  iinexg  4352  relimasn  5219  mapprc  7014  modom  7301  tz9.1c  7658  scott0  7802  scott0s  7804  cp  7807  karden  7811  acnrcl  7915  aceq3lem  7993  cff  8120  cff1  8130  cfss  8137  domtriomlem  8314  axdclem  8391  nqpr  8883  supmul  9968  hashf1lem2  11697  hashf1  11698  mreiincl  13813  efgval  15341  efger  15342  birthdaylem3  20784  disjex  24024  disjexc  24025  supadd  26229  mblfinlem2  26235  ismblfin  26237  itg2addnc  26249  sdclem1  26428  inisegn0  27099
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-v 2950  df-dif 3315  df-nul 3621
  Copyright terms: Public domain W3C validator