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

Theorem abn0 3803
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 3792 . 2  |-  ( { x  |  ph }  =/=  (/)  <->  E. x  x  e. 
{ x  |  ph } )
3 abid 2441 . . 3  |-  ( x  e.  { x  | 
ph }  <->  ph )
43exbii 1672 . 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 1617    e. wcel 1823   {cab 2439    =/= wne 2649   (/)c0 3783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-v 3108  df-dif 3464  df-nul 3784
This theorem is referenced by:  rabn0  3804  intexab  4595  iinexg  4597  relimasn  5348  mapprc  7416  modom  7713  tz9.1c  8152  scott0  8295  scott0s  8297  cp  8300  karden  8304  acnrcl  8414  aceq3lem  8492  cff  8619  cff1  8629  cfss  8636  domtriomlem  8813  axdclem  8890  nqpr  9381  supmul  10506  hashf1lem2  12489  hashf1  12490  mreiincl  15085  efgval  16934  efger  16935  birthdaylem3  23481  disjex  27662  disjexc  27663  mppsval  29196  supadd  30282  mblfinlem3  30293  ismblfin  30295  itg2addnc  30309  sdclem1  30476  inisegn0  31228  upbdrech  31744
  Copyright terms: Public domain W3C validator