Theorem rabeq0 4292

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

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 399  ∀wal 1536   = wceq 1538   ∈ wcel 2111  {cab 2776  ∀wral 3106  {crab 3110  ∅c0 4243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rab 3115  df-dif 3884  df-nul 4244

This theorem is referenced by:  rabn0  4293  rabnc  4295  dffr2  5484  frc  5485  frirr  5496  wereu2  5516  tz6.26  6147  fndmdifeq0  6791  fnnfpeq0  6917  wemapso2  9001  wemapwe  9144  hashbclem  13806  hashbc  13807  wrdnfi  13891  smuval2  15821  smupvallem  15822  smu01lem  15824  smumullem  15831  phiprmpw  16103  hashgcdeq  16116  prmreclem4  16245  cshws0  16427  pmtrsn  18639  efgsfo  18857  00lsp  19746  dsmm0cl  20429  ordthauslem  21988  pthaus  22243  xkohaus  22258  hmeofval  22363  mumul  25766  musum  25776  ppiub  25788  lgsquadlem2  25965  umgrnloop0  26902  lfgrnloop  26918  numedglnl  26937  usgrnloop0ALT  26995  lfuhgr1v0e  27044  nbuhgr  27133  nbumgr  27137  uhgrnbgr0nb  27144  nbgr0vtxlem  27145  vtxd0nedgb  27278  vtxdusgr0edgnelALT  27286  1loopgrnb0  27292  usgrvd0nedg  27323  vtxdginducedm1lem4  27332  wwlks  27621  iswwlksnon  27639  iswspthsnon  27642  0enwwlksnge1  27650  wspn0  27710  rusgr0edg  27759  clwwlk  27768  clwwlkn  27811  clwwlkn0  27813  clwwlknon  27875  clwwlknon1nloop  27884  clwwlknondisj  27896  vdn0conngrumgrv2  27981  eupth2lemb  28022  eulercrct  28027  frgrregorufr0  28109  numclwwlk3lem2  28169  ofldchr  30938  zarcls1  31222  measvuni  31583  dya2iocuni  31651  repr0  31992  reprlt  32000  reprgt  32002  nummin  32474  subfacp1lem6  32545  prv1n  32791  frpomin  33191  frpomin2  33192  poimirlem26  35083  poimirlem27  35084  cnambfre  35105  itg2addnclem2  35109  areacirclem5  35149  0dioph  39719  undisjrab  41010  supminfxr  42103  dvnprodlem3  42590  pimltmnf2  43336  pimconstlt0  43339  pimgtpnf2  43342  rmsupp0  44770  lcoc0  44831  rrxsphere  45162