Theorem rabeq0 3812

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 2913	. 2 |- ( A. x e. A -. ph <-> -. E. x e. A ph )
2		rabn0 3810	. . 3 |- ( { x e. A | ph } =/= (/) <-> E. x e. A ph )
3	2	necon1bbii 2731	. 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 1379   A.wral 2817   E.wrex 2818   {crab 2821   (/)c0 3790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-rab 2826  df-v 3120  df-dif 3484  df-nul 3791

This theorem is referenced by:  rabnc  3814  dffr2  4849  frc  4850  frirr  4861  wereu2  4881  fndmdifeq0  5993  fnnfpeq0  6102  wemapso2  7989  cantnfOLD  8144  wemapwe  8149  wemapweOLD  8150  hashbclem  12477  hashbc  12478  smuval2  14003  smupvallem  14004  smu01lem  14006  smumullem  14013  phiprmpw  14177  prmreclem4  14308  cshws0  14456  pmtrsn  16394  efgsfo  16607  00lsp  17475  dsmm0cl  18617  ordthauslem  19729  pthaus  19984  xkohaus  19999  hmeofval  20104  mumul  23298  musum  23310  ppiub  23322  lgsquadlem2  23473  usgranloop0  24171  usgra1v  24181  nbusgra  24219  nbgra0nb  24220  nbgra0edg  24223  cusgrasizeindslem2  24265  uvtx0  24282  clwwlkn0  24565  vdgr1b  24695  vdgr1a  24697  vdusgra0nedg  24699  usgravd0nedg  24709  eupath2  24771  vdn0frgrav2  24815  vdgn0frgrav2  24816  frgraregorufr0  24844  2spot0  24856  numclwwlkdisj  24872  numclwwlk3lem  24900  ofldchr  27597  measvuni  27978  dya2iocuni  28047  subfacp1lem6  28422  tz6.26  29180  cnambfre  29958  itg2addnclem2  29962  areacirclem5  30006  0dioph  30608  hashgcdeq  31055  rmsupp0  32335  lcoc0  32397