Theorem rabeq0 4394

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 4386	. 2 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		df-rab 3434	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
3	2	eqeq1i 2740	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅)
4		raln 3067	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
5	1, 3, 4	3bitr4i 303	1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395  ∀wal 1535   = wceq 1537   ∈ wcel 2106  {cab 2712  ∀wral 3059  {crab 3433  ∅c0 4339

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-cleq 2727  df-ral 3060  df-rab 3434  df-dif 3966  df-nul 4340

This theorem is referenced by:  rabn0  4395  rabnc  4397  dffr2ALT  5651  wereu2  5686  frpomin  6363  frpomin2  6364  tz6.26OLD  6371  fndmdifeq0  7064  fnnfpeq0  7198  wemapso2  9591  wemapwe  9735  hashbclem  14488  hashbc  14489  wrdnfi  14583  smuval2  16516  smupvallem  16517  smu01lem  16519  smumullem  16526  phiprmpw  16810  hashgcdeq  16823  prmreclem4  16953  cshws0  17136  pmtrsn  19552  efgsfo  19772  00lsp  20997  dsmm0cl  21778  ordthauslem  23407  pthaus  23662  xkohaus  23677  hmeofval  23782  mumul  27239  musum  27249  ppiub  27263  lgsquadlem2  27440  umgrnloop0  29141  lfgrnloop  29157  numedglnl  29176  usgrnloop0ALT  29237  lfuhgr1v0e  29286  nbuhgr  29375  nbumgr  29379  uhgrnbgr0nb  29386  nbgr0edglem  29388  vtxd0nedgb  29521  vtxdusgr0edgnelALT  29529  1loopgrnb0  29535  usgrvd0nedg  29566  vtxdginducedm1lem4  29575  wwlks  29865  iswwlksnon  29883  iswspthsnon  29886  0enwwlksnge1  29894  wspn0  29954  rusgr0edg  30003  clwwlk  30012  clwwlkn  30055  clwwlkn0  30057  clwwlknon  30119  clwwlknon1nloop  30128  clwwlknondisj  30140  vdn0conngrumgrv2  30225  eupth2lemb  30266  eulercrct  30271  frgrregorufr0  30353  numclwwlk3lem2  30413  ofldchr  33324  2sqr3minply  33753  zarcls1  33830  measvuni  34195  dya2iocuni  34265  repr0  34605  reprlt  34613  reprgt  34615  nummin  35084  subfacp1lem6  35170  prv1n  35416  poimirlem26  37633  poimirlem27  37634  cnambfre  37655  itg2addnclem2  37659  areacirclem5  37699  sticksstones1  42128  nna4b4nsq  42647  0dioph  42766  undisjrab  44302  supminfxr  45414  dvnprodlem3  45904  pimltmnf2f  46653  pimconstlt0  46657  pimgtpnf2f  46661  isubgr0uhgr  47797  stgr0  47863  rmsupp0  48213  lcoc0  48268  rrxsphere  48598