Theorem rabeq0 4342

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 4333	. 2 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		df-rab 3415	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
3	2	eqeq1i 2767	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅)
4		raln 3085	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
5	1, 3, 4	3bitr4i 305	1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 208   ∧ wa 399  ∀wal 1558   = wceq 1560   ∈ wcel 2142  {cab 2740  ∀wral 3076  {crab 3414  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-clab 2741  df-cleq 2754  df-ral 3077  df-rab 3415  df-dif 3907  df-nul 4286

This theorem is referenced by:  rabn0  4343  rabnc  4345  dffr2ALT  5609  wereu2  5644  frpomin  6327  frpomin2  6328  fndmdifeq0  7025  fnnfpeq0  7162  wemapso2  9501  wemapwe  9652  hashbclem  14465  hashbc  14466  wrdnfi  14561  smuval2  16516  smupvallem  16517  smu01lem  16519  smumullem  16526  phiprmpw  16811  hashgcdeq  16825  prmreclem4  16955  cshws0  17137  pmtrsn  19559  efgsfo  19779  00lsp  21045  ofldchr  21625  dsmm0cl  21789  ordthauslem  23440  pthaus  23695  xkohaus  23710  hmeofval  23815  mumul  27242  musum  27252  ppiub  27265  lgsquadlem2  27442  umgrnloop0  29307  lfgrnloop  29323  numedglnl  29342  usgrnloop0ALT  29403  lfuhgr1v0e  29452  nbuhgr  29541  nbumgr  29545  uhgrnbgr0nb  29552  nbgr0edglem  29554  vtxd0nedgb  29686  vtxdusgr0edgnelALT  29694  1loopgrnb0  29700  usgrvd0nedg  29731  vtxdginducedm1lem4  29740  wwlks  30032  iswwlksnon  30050  iswspthsnon  30053  0enwwlksnge1  30061  wspn0  30121  rusgr0edg  30173  clwwlk  30182  clwwlkn  30225  clwwlkn0  30227  clwwlknon  30289  clwwlknon1nloop  30298  clwwlknondisj  30310  vdn0conngrumgrv2  30395  eupth2lemb  30436  eulercrct  30441  frgrregorufr0  30523  numclwwlk3lem2  30583  esplyfval2  33859  2sqr3minply  34074  cos9thpiminply  34082  zarcls1  34163  measvuni  34508  dya2iocuni  34577  repr0  34902  reprlt  34910  reprgt  34912  nummin  35386  fineqvnttrclselem1  35414  subfacp1lem6  35532  prv1n  35778  poimirlem26  38142  poimirlem27  38143  cnambfre  38164  itg2addnclem2  38168  areacirclem5  38208  sticksstones1  42760  nna4b4nsq  43239  0dioph  43356  undisjrab  44879  supminfxr  46035  dvnprodlem3  46519  pimltmnf2f  47268  pimconstlt0  47272  pimgtpnf2f  47276  isubgr0uhgr  48492  stgr0  48579  rmsupp0  48987  lcoc0  49041  rrxsphere  49367