Theorem rabeq0 4351

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	⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑)

Proof of Theorem rabeq0

Step	Hyp	Ref	Expression
1		ab0 4343	. 2 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		df-rab 3406	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
3	2	eqeq1i 2734	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅)
4		raln 3052	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
5	1, 3, 4	3bitr4i 303	1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395  ∀wal 1538   = wceq 1540   ∈ wcel 2109  {cab 2707  ∀wral 3044  {crab 3405  ∅c0 4296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-ral 3045  df-rab 3406  df-dif 3917  df-nul 4297

This theorem is referenced by:  rabn0  4352  rabnc  4354  dffr2ALT  5600  wereu2  5635  frpomin  6313  frpomin2  6314  fndmdifeq0  7016  fnnfpeq0  7152  wemapso2  9506  wemapwe  9650  hashbclem  14417  hashbc  14418  wrdnfi  14513  smuval2  16452  smupvallem  16453  smu01lem  16455  smumullem  16462  phiprmpw  16746  hashgcdeq  16760  prmreclem4  16890  cshws0  17072  pmtrsn  19449  efgsfo  19669  00lsp  20887  dsmm0cl  21649  ordthauslem  23270  pthaus  23525  xkohaus  23540  hmeofval  23645  mumul  27091  musum  27101  ppiub  27115  lgsquadlem2  27292  umgrnloop0  29036  lfgrnloop  29052  numedglnl  29071  usgrnloop0ALT  29132  lfuhgr1v0e  29181  nbuhgr  29270  nbumgr  29274  uhgrnbgr0nb  29281  nbgr0edglem  29283  vtxd0nedgb  29416  vtxdusgr0edgnelALT  29424  1loopgrnb0  29430  usgrvd0nedg  29461  vtxdginducedm1lem4  29470  wwlks  29765  iswwlksnon  29783  iswspthsnon  29786  0enwwlksnge1  29794  wspn0  29854  rusgr0edg  29903  clwwlk  29912  clwwlkn  29955  clwwlkn0  29957  clwwlknon  30019  clwwlknon1nloop  30028  clwwlknondisj  30040  vdn0conngrumgrv2  30125  eupth2lemb  30166  eulercrct  30171  frgrregorufr0  30253  numclwwlk3lem2  30313  ofldchr  33292  2sqr3minply  33770  cos9thpiminply  33778  zarcls1  33859  measvuni  34204  dya2iocuni  34274  repr0  34602  reprlt  34610  reprgt  34612  nummin  35081  subfacp1lem6  35172  prv1n  35418  poimirlem26  37640  poimirlem27  37641  cnambfre  37662  itg2addnclem2  37666  areacirclem5  37706  sticksstones1  42134  nna4b4nsq  42648  0dioph  42766  undisjrab  44295  supminfxr  45460  dvnprodlem3  45946  pimltmnf2f  46695  pimconstlt0  46699  pimgtpnf2f  46703  isubgr0uhgr  47873  stgr0  47959  rmsupp0  48356  lcoc0  48411  rrxsphere  48737