Theorem rabeq0 3770

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 2852	. 2 |- ( A. x e. A -. ph <-> -. E. x e. A ph )
2		rabn0 3768	. . 3 |- ( { x e. A | ph } =/= (/) <-> E. x e. A ph )
3	2	necon1bbii 2716	. 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 1370   A.wral 2799   E.wrex 2800   {crab 2803   (/)c0 3748

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2804  df-rex 2805  df-rab 2808  df-v 3080  df-dif 3442  df-nul 3749

This theorem is referenced by:  rabnc  3772  dffr2  4796  frc  4797  frirr  4808  wereu2  4828  fndmdifeq0  5921  fnnfpeq0  6021  wemapso2  7883  cantnfOLD  8038  wemapwe  8043  wemapweOLD  8044  hashbclem  12327  hashbc  12328  smuval2  13800  smupvallem  13801  smu01lem  13803  smumullem  13810  phiprmpw  13973  prmreclem4  14102  cshws0  14250  pmtrsn  16148  efgsfo  16361  00lsp  17195  dsmm0cl  18300  ordthauslem  19129  pthaus  19353  xkohaus  19368  hmeofval  19473  mumul  22662  musum  22674  ppiub  22686  lgsquadlem2  22837  usgranloop0  23478  usgra1v  23487  nbusgra  23518  nbgra0nb  23519  nbgra0edg  23522  cusgrasizeindslem2  23561  uvtx0  23578  vdgr1b  23753  vdgr1a  23755  vdusgra0nedg  23757  usgravd0nedg  23761  eupath2  23780  ofldchr  26450  measvuni  26796  dya2iocuni  26865  subfacp1lem6  27240  tz6.26  27833  cnambfre  28611  itg2addnclem2  28615  areacirclem5  28659  0dioph  29288  hashgcdeq  29737  clwwlkn0  30608  vdn0frgrav2  30787  vdgn0frgrav2  30788  frgraregorufr0  30816  2spot0  30828  numclwwlkdisj  30844  numclwwlk3lem  30872  rmsupp0  30952  lcoc0  31111