Theorem rabeq0 3734

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 2828	. 2 |- ( A. x e. A -. ph <-> -. E. x e. A ph )
2		rabn0 3732	. . 3 |- ( { x e. A | ph } =/= (/) <-> E. x e. A ph )
3	2	necon1bbii 2646	. 2 |- ( -. E. x e. A ph <-> { x e. A | ph } = (/) )
4	1, 3	bitr2i 250	1 |- ( { x e. A | ph } = (/) <-> A. x e. A -. ph )

Syntax hints:   -. wn 3   <-> wb 184   = wceq 1399   A.wral 2732   E.wrex 2733   {crab 2736   (/)c0 3711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-dif 3392  df-nul 3712

This theorem is referenced by:  rabnc  3736  dffr2  4758  frc  4759  frirr  4770  wereu2  4790  fndmdifeq0  5895  fnnfpeq0  6004  wemapso2  7894  cantnfOLD  8047  wemapwe  8052  wemapweOLD  8053  hashbclem  12405  hashbc  12406  smuval2  14134  smupvallem  14135  smu01lem  14137  smumullem  14144  phiprmpw  14308  prmreclem4  14439  cshws0  14588  pmtrsn  16661  efgsfo  16874  00lsp  17740  dsmm0cl  18862  ordthauslem  19970  pthaus  20224  xkohaus  20239  hmeofval  20344  mumul  23572  musum  23584  ppiub  23596  lgsquadlem2  23747  usgranloop0  24501  usgra1v  24511  nbusgra  24549  nbgra0nb  24550  nbgra0edg  24553  cusgrasizeindslem2  24595  uvtx0  24612  clwwlkn0  24895  vdgr1b  25025  vdgr1a  25027  vdusgra0nedg  25029  usgravd0nedg  25039  eupath2  25101  vdn0frgrav2  25144  vdgn0frgrav2  25145  frgraregorufr0  25173  2spot0  25185  numclwwlkdisj  25201  numclwwlk3lem  25229  ofldchr  27958  measvuni  28341  dya2iocuni  28410  subfacp1lem6  28818  tz6.26  29450  cnambfre  30228  itg2addnclem2  30233  areacirclem5  30277  0dioph  30877  hashgcdeq  31326  undisjrab  31354  dvnprodlem3  31911  rmsupp0  33161  lcoc0  33223