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

Theorem rabeq0 3649
Description: Condition for a restricted class abstraction to be empty. (Contributed by Jeff Madsen, 7-Jun-2010.)
Assertion
Ref Expression
rabeq0  |-  ( { x  e.  A  |  ph }  =  (/)  <->  A. x  e.  A  -.  ph )

Proof of Theorem rabeq0
StepHypRef Expression
1 ralnex 2715 . 2  |-  ( A. x  e.  A  -.  ph  <->  -. 
E. x  e.  A  ph )
2 rabn0 3647 . . 3  |-  ( { x  e.  A  |  ph }  =/=  (/)  <->  E. x  e.  A  ph )
32necon1bbii 2656 . 2  |-  ( -. 
E. x  e.  A  ph  <->  { x  e.  A  |  ph }  =  (/) )
41, 3bitr2i 242 1  |-  ( { x  e.  A  |  ph }  =  (/)  <->  A. x  e.  A  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 177    = wceq 1652   A.wral 2705   E.wrex 2706   {crab 2709   (/)c0 3628
This theorem is referenced by:  rabnc  3651  rabrsn  3874  dffr2  4547  frc  4548  frirr  4559  wereu2  4579  fndmdifeq0  5836  cantnf  7649  wemapwe  7654  hashbclem  11701  hashbc  11702  smuval2  12994  smupvallem  12995  smu01lem  12997  smumullem  13004  phiprmpw  13165  prmreclem4  13287  efgsfo  15371  00lsp  16057  ordthauslem  17447  pthaus  17670  xkohaus  17685  hmeofval  17790  mumul  20964  musum  20976  ppiub  20988  lgsquadlem2  21139  usgranloop0  21400  usgra1v  21409  nbusgra  21440  nbgra0nb  21441  nbgra0edg  21444  cusgrasizeindslem2  21483  uvtx0  21500  vdgr1b  21675  vdgr1a  21677  vdusgra0nedg  21679  usgravd0nedg  21683  eupath2  21702  ofldchr  24244  measvuni  24568  dya2iocuni  24633  subfacp1lem6  24871  tz6.26  25480  cnambfre  26255  itg2addnclem2  26257  areacirclem5  26296  fnnfpeq0  26739  0dioph  26837  dsmm0cl  27183  hashgcdeq  27494  vdn0frgrav2  28414  vdgn0frgrav2  28415  frgraregorufr0  28441  2spot0  28453
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 2417
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 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2958  df-dif 3323  df-nul 3629
  Copyright terms: Public domain W3C validator