Theorem rabeq0 3757

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 2834	. 2 |- ( A. x e. A -. ph <-> -. E. x e. A ph )
2		rabn0 3755	. . 3 |- ( { x e. A | ph } =/= (/) <-> E. x e. A ph )
3	2	necon1bbii 2692	. 2 |- ( -. E. x e. A ph <-> { x e. A | ph } = (/) )
4	1, 3	bitr2i 258	1 |- ( { x e. A | ph } = (/) <-> A. x e. A -. ph )

Syntax hints:   -. wn 3   <-> wb 189   = wceq 1452   A.wral 2756   E.wrex 2757   {crab 2760   (/)c0 3722

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-dif 3393  df-nul 3723

This theorem is referenced by:  rabnc  3759  dffr2  4804  frc  4805  frirr  4816  wereu2  4836  tz6.26  5418  fndmdifeq0  6003  fnnfpeq0  6111  wemapso2  8086  wemapwe  8220  hashbclem  12656  hashbc  12657  smuval2  14535  smupvallem  14536  smu01lem  14538  smumullem  14545  phiprmpw  14803  prmreclem4  14942  cshws0  15150  pmtrsn  17238  efgsfo  17467  00lsp  18282  dsmm0cl  19380  ordthauslem  20476  pthaus  20730  xkohaus  20745  hmeofval  20850  mumul  24187  musum  24199  ppiub  24211  lgsquadlem2  24362  usgranloop0  25186  usgra1v  25196  nbusgra  25235  nbgra0nb  25236  nbgra0edg  25239  cusgrasizeindslem2  25281  uvtx0  25298  clwwlkn0  25581  vdgr1b  25711  vdgr1a  25713  vdusgra0nedg  25715  usgravd0nedg  25725  eupath2  25787  vdn0frgrav2  25830  vdgn0frgrav2  25831  frgraregorufr0  25859  2spot0  25871  numclwwlkdisj  25887  numclwwlk3lem  25915  ofldchr  28651  measvuni  29110  dya2iocuni  29178  subfacp1lem6  29980  poimirlem26  32030  poimirlem27  32031  cnambfre  32053  itg2addnclem2  32058  areacirclem5  32100  0dioph  35692  hashgcdeq  36146  undisjrab  36724  dvnprodlem3  37920  umgrnloop0  39354  lfgrnloop  39370  usgrnloop0ALT  39450  usgr1vr  39493  nbuhgr  39575  nbumgr  39579  uhgrnbgr0nb  39586  nbgr0vtxlem  39587  vtxd0nedgb  39711  vtxdusgr0edgnelALT  39719  1loopgrnb0  39724  usgrvd0nedg  39756  eupth2lemb  40149  eulercrct  40154  rmsupp0  40661  lcoc0  40723