Theorem rabeq0 3957

Description: Condition for a restricted class abstraction to be empty. (Contributed by Jeff Madsen, 7-Jun-2010.) (Revised by BJ, 16-Jul-2021.)

Assertion

Ref	Expression
rabeq0	|- ( { x e. A | ph } = (/) <-> A. x e. A -. ph )

Proof of Theorem rabeq0

Step	Hyp	Ref	Expression
1		ab0 3951	. 2 |- ( { x | ( x e. A /\ ph ) } = (/) <-> A. x -. ( x e. A /\ ph ) )
2		df-rab 2921	. . 3 |- { x e. A | ph } = { x | ( x e. A /\ ph ) }
3	2	eqeq1i 2627	. 2 |- ( { x e. A | ph } = (/) <-> { x | ( x e. A /\ ph ) } = (/) )
4		raln 2991	. 2 |- ( A. x e. A -. ph <-> A. x -. ( x e. A /\ ph ) )
5	1, 3, 4	3bitr4i 292	1 |- ( { x e. A | ph } = (/) <-> A. x e. A -. ph )

Syntax hints:   -. wn 3   <-> wb 196   /\ wa 384   A.wal 1481   = wceq 1483   e. wcel 1990   {cab 2608   A.wral 2912   {crab 2916   (/)c0 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rab 2921  df-v 3202  df-dif 3577  df-nul 3916

This theorem is referenced by:  rabn0  3958  rabnc  3962  dffr2  5079  frc  5080  frirr  5091  wereu2  5111  tz6.26  5711  fndmdifeq0  6323  fnnfpeq0  6444  wemapso2  8458  wemapwe  8594  hashbclem  13236  hashbc  13237  smuval2  15204  smupvallem  15205  smu01lem  15207  smumullem  15214  phiprmpw  15481  hashgcdeq  15494  prmreclem4  15623  cshws0  15808  pmtrsn  17939  efgsfo  18152  00lsp  18981  dsmm0cl  20084  ordthauslem  21187  pthaus  21441  xkohaus  21456  hmeofval  21561  mumul  24907  musum  24917  ppiub  24929  lgsquadlem2  25106  umgrnloop0  26004  lfgrnloop  26020  numedglnl  26039  usgrnloop0ALT  26097  lfuhgr1v0e  26146  nbuhgr  26239  nbumgr  26243  uhgrnbgr0nb  26250  nbgr0vtxlem  26251  vtxd0nedgb  26384  vtxdusgr0edgnelALT  26392  1loopgrnb0  26398  usgrvd0nedg  26429  vtxdginducedm1lem4  26438  wwlks  26727  0enwwlksnge1  26749  wspn0  26820  rusgr0edg  26868  clwwlks  26879  clwwlksndisj  26973  vdn0conngrumgrv2  27056  eupth2lemb  27097  eulercrct  27102  frgrregorufr0  27188  numclwwlk3lem  27241  ofldchr  29814  measvuni  30277  dya2iocuni  30345  repr0  30689  reprlt  30697  reprgt  30699  subfacp1lem6  31167  poimirlem26  33435  poimirlem27  33436  cnambfre  33458  itg2addnclem2  33462  areacirclem5  33504  0dioph  37342  undisjrab  38505  supminfxr  39694  dvnprodlem3  40163  pimltmnf2  40911  pimconstlt0  40914  pimgtpnf2  40917  rmsupp0  42149  lcoc0  42211