Theorem rabeq0 3753

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

Step	Hyp	Ref	Expression
1		ralnex 2833	. 2 |- ( A. x e. A -. ph <-> -. E. x e. A ph )
2		rabn0 3751	. . 3 |- ( { x e. A | ph } =/= (/) <-> E. x e. A ph )
3	2	necon1bbii 2672	. 2 |- ( -. E. x e. A ph <-> { x e. A | ph } = (/) )
4	1, 3	bitr2i 254	1 |- ( { x e. A | ph } = (/) <-> A. x e. A -. ph )

Syntax hints:   -. wn 3   <-> wb 188   = wceq 1443   A.wral 2736   E.wrex 2737   {crab 2740   (/)c0 3730

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3046  df-dif 3406  df-nul 3731

This theorem is referenced by:  rabnc  3755  dffr2  4798  frc  4799  frirr  4810  wereu2  4830  tz6.26  5410  fndmdifeq0  5986  fnnfpeq0  6093  wemapso2  8065  wemapwe  8199  hashbclem  12612  hashbc  12613  smuval2  14449  smupvallem  14450  smu01lem  14452  smumullem  14459  phiprmpw  14717  prmreclem4  14856  cshws0  15065  pmtrsn  17153  efgsfo  17382  00lsp  18197  dsmm0cl  19296  ordthauslem  20392  pthaus  20646  xkohaus  20661  hmeofval  20766  mumul  24101  musum  24113  ppiub  24125  lgsquadlem2  24276  usgranloop0  25100  usgra1v  25110  nbusgra  25149  nbgra0nb  25150  nbgra0edg  25153  cusgrasizeindslem2  25195  uvtx0  25212  clwwlkn0  25495  vdgr1b  25625  vdgr1a  25627  vdusgra0nedg  25629  usgravd0nedg  25639  eupath2  25701  vdn0frgrav2  25744  vdgn0frgrav2  25745  frgraregorufr0  25773  2spot0  25785  numclwwlkdisj  25801  numclwwlk3lem  25829  ofldchr  28570  measvuni  29029  dya2iocuni  29098  subfacp1lem6  29901  poimirlem26  31959  poimirlem27  31960  cnambfre  31982  itg2addnclem2  31987  areacirclem5  32029  0dioph  35615  hashgcdeq  36069  undisjrab  36648  dvnprodlem3  37817  umgrnloop0  39183  usgrnloop0ALT  39274  usgr1vr  39312  nbuhgr  39394  nbumgr  39398  uhgrnbgr0nb  39405  nbgr0vtxlem  39406  uhgrvd0nedgb  39528  vtxdusgr0edgnelALT  39533  uspgrloopnb0  39539  usgrvd0nedg  39553  rmsupp0  40140  lcoc0  40202