Theorem rabeq0 3647

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 2715	. 2 |- ( A. x e. A -. ph <-> -. E. x e. A ph )
2		rabn0 3645	. . 3 |- ( { x e. A | ph } =/= (/) <-> E. x e. A ph )
3	2	necon1bbii 2653	. 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 1362   A.wral 2705   E.wrex 2706   {crab 2709   (/)c0 3625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-nul 3626

This theorem is referenced by:  rabnc  3649  dffr2  4672  frc  4673  frirr  4684  wereu2  4704  fndmdifeq0  5797  fnnfpeq0  5896  wemapso2  7756  cantnfOLD  7911  wemapwe  7916  wemapweOLD  7917  hashbclem  12189  hashbc  12190  smuval2  13661  smupvallem  13662  smu01lem  13664  smumullem  13671  phiprmpw  13834  prmreclem4  13963  cshws0  14111  efgsfo  16216  00lsp  16984  dsmm0cl  18007  ordthauslem  18829  pthaus  19053  xkohaus  19068  hmeofval  19173  mumul  22404  musum  22416  ppiub  22428  lgsquadlem2  22579  usgranloop0  23122  usgra1v  23131  nbusgra  23162  nbgra0nb  23163  nbgra0edg  23166  cusgrasizeindslem2  23205  uvtx0  23222  vdgr1b  23397  vdgr1a  23399  vdusgra0nedg  23401  usgravd0nedg  23405  eupath2  23424  ofldchr  26135  measvuni  26482  dya2iocuni  26552  subfacp1lem6  26921  tz6.26  27513  cnambfre  28284  itg2addnclem2  28288  areacirclem5  28332  0dioph  28962  hashgcdeq  29411  clwwlkn0  30283  vdn0frgrav2  30462  vdgn0frgrav2  30463  frgraregorufr0  30491  2spot0  30503  numclwwlkdisj  30519  numclwwlk3lem  30547  pmtrsn  30601  rmsupp0  30612  lcoc0  30665