Theorem rabeq0 4187

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 4182	. 2 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		df-rab 3099	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
3	2	eqeq1i 2783	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅)
4		raln 3173	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
5	1, 3, 4	3bitr4i 295	1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 198   ∧ wa 386  ∀wal 1599   = wceq 1601   ∈ wcel 2107  {cab 2763  ∀wral 3090  {crab 3094  ∅c0 4141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rab 3099  df-dif 3795  df-nul 4142

This theorem is referenced by:  rabn0  4188  rabnc  4190  dffr2  5320  frc  5321  frirr  5332  wereu2  5352  tz6.26  5964  fndmdifeq0  6586  fnnfpeq0  6711  wemapso2  8747  wemapwe  8891  hashbclem  13550  hashbc  13551  wrdnfi  13637  smuval2  15610  smupvallem  15611  smu01lem  15613  smumullem  15620  phiprmpw  15885  hashgcdeq  15898  prmreclem4  16027  cshws0  16207  pmtrsn  18323  efgsfo  18537  00lsp  19376  dsmm0cl  20483  ordthauslem  21595  pthaus  21850  xkohaus  21865  hmeofval  21970  mumul  25359  musum  25369  ppiub  25381  lgsquadlem2  25558  umgrnloop0  26457  lfgrnloop  26473  numedglnl  26493  usgrnloop0ALT  26551  lfuhgr1v0e  26601  nbuhgr  26690  nbumgr  26694  uhgrnbgr0nb  26701  nbgr0vtxlem  26702  vtxd0nedgb  26836  vtxdusgr0edgnelALT  26844  1loopgrnb0  26850  usgrvd0nedg  26881  vtxdginducedm1lem4  26890  wwlks  27184  iswwlksnon  27202  iswspthsnon  27205  0enwwlksnge1  27213  wspn0  27304  rusgr0edg  27353  clwwlk  27363  clwwlkn  27415  clwwlkn0  27417  clwwlknon  27492  clwwlknon1nloop  27501  clwwlknondisj  27513  vdn0conngrumgrv2  27599  eupth2lemb  27641  eulercrct  27646  frgrregorufr0  27732  numclwwlk3lem2  27816  ofldchr  30376  measvuni  30875  dya2iocuni  30943  repr0  31291  reprlt  31299  reprgt  31301  subfacp1lem6  31766  frpomin  32327  frpomin2  32328  poimirlem26  34061  poimirlem27  34062  cnambfre  34083  itg2addnclem2  34087  areacirclem5  34129  0dioph  38302  undisjrab  39461  supminfxr  40599  dvnprodlem3  41091  pimltmnf2  41838  pimconstlt0  41841  pimgtpnf2  41844  rmsupp0  43164  lcoc0  43226  rrxsphere  43484