Theorem rabeq0 4385

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

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 395  ∀wal 1532   = wceq 1534   ∈ wcel 2099  {cab 2705  ∀wral 3058  {crab 3429  ∅c0 4323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2706  df-cleq 2720  df-ral 3059  df-rab 3430  df-dif 3950  df-nul 4324

This theorem is referenced by:  rabn0  4386  rabnc  4388  dffr2ALT  5643  wereu2  5675  frpomin  6346  frpomin2  6347  tz6.26OLD  6354  fndmdifeq0  7053  fnnfpeq0  7187  wemapso2  9577  wemapwe  9721  hashbclem  14444  hashbc  14445  wrdnfi  14531  smuval2  16457  smupvallem  16458  smu01lem  16460  smumullem  16467  phiprmpw  16745  hashgcdeq  16758  prmreclem4  16888  cshws0  17071  pmtrsn  19474  efgsfo  19694  00lsp  20865  dsmm0cl  21674  ordthauslem  23300  pthaus  23555  xkohaus  23570  hmeofval  23675  mumul  27126  musum  27136  ppiub  27150  lgsquadlem2  27327  umgrnloop0  28935  lfgrnloop  28951  numedglnl  28970  usgrnloop0ALT  29031  lfuhgr1v0e  29080  nbuhgr  29169  nbumgr  29173  uhgrnbgr0nb  29180  nbgr0vtxlem  29181  vtxd0nedgb  29315  vtxdusgr0edgnelALT  29323  1loopgrnb0  29329  usgrvd0nedg  29360  vtxdginducedm1lem4  29369  wwlks  29659  iswwlksnon  29677  iswspthsnon  29680  0enwwlksnge1  29688  wspn0  29748  rusgr0edg  29797  clwwlk  29806  clwwlkn  29849  clwwlkn0  29851  clwwlknon  29913  clwwlknon1nloop  29922  clwwlknondisj  29934  vdn0conngrumgrv2  30019  eupth2lemb  30060  eulercrct  30065  frgrregorufr0  30147  numclwwlk3lem2  30207  ofldchr  33042  zarcls1  33470  measvuni  33833  dya2iocuni  33903  repr0  34243  reprlt  34251  reprgt  34253  nummin  34714  subfacp1lem6  34795  prv1n  35041  poimirlem26  37119  poimirlem27  37120  cnambfre  37141  itg2addnclem2  37145  areacirclem5  37185  sticksstones1  41618  nna4b4nsq  42084  0dioph  42198  undisjrab  43743  supminfxr  44846  dvnprodlem3  45336  pimltmnf2f  46085  pimconstlt0  46089  pimgtpnf2f  46093  rmsupp0  47432  lcoc0  47490  rrxsphere  47821