Theorem rabeq0 3807

Description: Condition for a restricted class abstraction to be empty. (Contributed by Jeff Madsen, 7-Jun-2010.)

Assertion

Ref	Expression
rabeq0

Proof of Theorem rabeq0

Step	Hyp	Ref	Expression
1		ralnex 2903	. 2
2		rabn0 3805	. . 3
3	2	necon1bbii 2721	. 2
4	1, 3	bitr2i 250	1

Syntax hints:  -.wn 3  <->wb 184  =wceq 1395  A.wral 2807  E.wrex 2808  {crab 2811  c0 3784

This theorem is referenced by:  rabnc  3809  dffr2  4849  frc  4850  frirr  4861  wereu2  4881  fndmdifeq0  5993  fnnfpeq0  6102  wemapso2  8000  cantnfOLD  8155  wemapwe  8160  wemapweOLD  8161  hashbclem  12501  hashbc  12502  smuval2  14132  smupvallem  14133  smu01lem  14135  smumullem  14142  phiprmpw  14306  prmreclem4  14437  cshws0  14586  pmtrsn  16544  efgsfo  16757  00lsp  17627  dsmm0cl  18771  ordthauslem  19884  pthaus  20139  xkohaus  20154  hmeofval  20259  mumul  23455  musum  23467  ppiub  23479  lgsquadlem2  23630  usgranloop0  24380  usgra1v  24390  nbusgra  24428  nbgra0nb  24429  nbgra0edg  24432  cusgrasizeindslem2  24474  uvtx0  24491  clwwlkn0  24774  vdgr1b  24904  vdgr1a  24906  vdusgra0nedg  24908  usgravd0nedg  24918  eupath2  24980  vdn0frgrav2  25023  vdgn0frgrav2  25024  frgraregorufr0  25052  2spot0  25064  numclwwlkdisj  25080  numclwwlk3lem  25108  ofldchr  27804  measvuni  28185  dya2iocuni  28254  subfacp1lem6  28629  tz6.26  29285  cnambfre  30063  itg2addnclem2  30067  areacirclem5  30111  0dioph  30712  hashgcdeq  31158  undisjrab  31186  dvnprodlem3  31745  rmsupp0  32961  lcoc0  33023

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-nul 3785