Theorem rabeq0 3789

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 2887	. 2 |- ( A. x e. A -. ph <-> -. E. x e. A ph )
2		rabn0 3787	. . 3 |- ( { x e. A | ph } =/= (/) <-> E. x e. A ph )
3	2	necon1bbii 2705	. 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 1381   A.wral 2791   E.wrex 2792   {crab 2795   (/)c0 3767

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-dif 3461  df-nul 3768

This theorem is referenced by:  rabnc  3791  dffr2  4830  frc  4831  frirr  4842  wereu2  4862  fndmdifeq0  5974  fnnfpeq0  6083  wemapso2  7977  cantnfOLD  8132  wemapwe  8137  wemapweOLD  8138  hashbclem  12475  hashbc  12476  smuval2  14004  smupvallem  14005  smu01lem  14007  smumullem  14014  phiprmpw  14178  prmreclem4  14309  cshws0  14458  pmtrsn  16413  efgsfo  16626  00lsp  17495  dsmm0cl  18638  ordthauslem  19750  pthaus  20005  xkohaus  20020  hmeofval  20125  mumul  23320  musum  23332  ppiub  23344  lgsquadlem2  23495  usgranloop0  24245  usgra1v  24255  nbusgra  24293  nbgra0nb  24294  nbgra0edg  24297  cusgrasizeindslem2  24339  uvtx0  24356  clwwlkn0  24639  vdgr1b  24769  vdgr1a  24771  vdusgra0nedg  24773  usgravd0nedg  24783  eupath2  24845  vdn0frgrav2  24888  vdgn0frgrav2  24889  frgraregorufr0  24917  2spot0  24929  numclwwlkdisj  24945  numclwwlk3lem  24973  ofldchr  27670  measvuni  28051  dya2iocuni  28120  subfacp1lem6  28495  tz6.26  29253  cnambfre  30031  itg2addnclem2  30035  areacirclem5  30079  0dioph  30680  hashgcdeq  31127  undisjrab  31155  rmsupp0  32671  lcoc0  32733