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

Theorem abn0 3767
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 2618 . . 3  |-  F/_ x { x  |  ph }
21n0f 3756 . 2  |-  ( { x  |  ph }  =/=  (/)  <->  E. x  x  e. 
{ x  |  ph } )
3 abid 2441 . . 3  |-  ( x  e.  { x  | 
ph }  <->  ph )
43exbii 1635 . 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 1587    e. wcel 1758   {cab 2439    =/= wne 2648   (/)c0 3748
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-v 3080  df-dif 3442  df-nul 3749
This theorem is referenced by:  rabn0  3768  intexab  4561  iinexg  4563  relimasn  5303  mapprc  7331  modom  7627  tz9.1c  8064  scott0  8207  scott0s  8209  cp  8212  karden  8216  acnrcl  8326  aceq3lem  8404  cff  8531  cff1  8541  cfss  8548  domtriomlem  8725  axdclem  8802  nqpr  9297  supmul  10412  hashf1lem2  12330  hashf1  12331  mreiincl  14656  efgval  16338  efger  16339  birthdaylem3  22483  disjex  26105  disjexc  26106  supadd  28586  mblfinlem3  28598  ismblfin  28600  itg2addnc  28614  sdclem1  28807  inisegn0  29564
  Copyright terms: Public domain W3C validator