Theorem rabeq0 4338

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 4329	. 2 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		df-rab 3414	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
3	2	eqeq1i 2766	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅)
4		raln 3086	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
5	1, 3, 4	3bitr4i 306	1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570   ∈ wcel 2145  {cab 2739  ∀wral 3077  {crab 3413  ∅c0 4279

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2740  df-cleq 2753  df-ral 3078  df-rab 3414  df-dif 3902  df-nul 4280

This theorem is used by:  rabn0  4339  rabnc  4341  dffr2ALT  5613  wereu2  5648  frpomin  6342  frpomin2  6343  fndmdifeq0  7041  fnnfpeq0  7181  wemapso2  9540  wemapwe  9691  hashbclem  14590  hashbc  14591  wrdnfi  14686  smuval2  16645  smupvallem  16646  smu01lem  16648  smumullem  16655  phiprmpw  16946  hashgcdeq  16960  prmreclem4  17090  cshws0  17272  pmtrsn  19726  efgsfo  19946  00lsp  21249  ofldchr  21875  dsmm0cl  22039  ordthauslem  23694  pthaus  23950  xkohaus  23965  hmeofval  24070  mumul  27501  musum  27511  ppiub  27524  lgsquadlem2  27701  nna4b4nsq  27983  umgrnloop0  29680  lfgrnloop  29696  numedglnl  29715  usgrnloop0ALT  29779  lfuhgr1v0e  29828  nbuhgr  29917  nbumgr  29921  uhgrnbgr0nb  29928  nbgr0edglem  29930  vtxd0nedgb  30062  vtxdusgr0edgnelALT  30070  1loopgrnb0  30076  usgrvd0nedg  30107  vtxdginducedm1lem4  30116  wwlks  30417  iswwlksnon  30435  iswspthsnon  30438  0enwwlksnge1  30446  wspn0  30506  rusgr0edg  30558  clwwlk  30567  clwwlkn  30610  clwwlkn0  30612  clwwlknon  30674  clwwlknon1nloop  30683  clwwlknondisj  30695  vdn0conngrumgrv2  30790  eupth2lemb  30831  eulercrct  30836  frgrregorufr0  30918  numclwwlk3lem2  30978  esplyfval2  34190  2sqr3minply  34405  cos9thpiminply  34413  zarcls1  34494  measvuni  34840  dya2iocuni  34908  repr0  35233  reprlt  35241  reprgt  35243  nummin  35711  fineqvnttrclselem1  35772  subfacp1lem6  35929  prv1n  36175  poimirlem26  38544  poimirlem27  38545  cnambfre  38566  itg2addnclem2  38570  areacirclem5  38610  sticksstones1  43176  frlmnzcoordex  43632  0dioph  43768  undisjrab  45275  supminfxr  46443  dvnprodlem3  46927  pimltmnf2f  47676  pimconstlt0  47680  pimgtpnf2f  47684  isubgr0uhgr  48940  stgr0  49027  rmsupp0  49449  lcoc0  49503  rrxsphere  49829