Theorem rabeq0 4324

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

Syntax hints:  ¬ wn 3   ↔ wb 208   ∧ wa 398  ∀wal 1535   = wceq 1537   ∈ wcel 2114  {cab 2799  ∀wral 3138  {crab 3142  ∅c0 4279

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rab 3147  df-dif 3927  df-nul 4280

This theorem is referenced by:  rabn0  4325  rabnc  4327  dffr2  5506  frc  5507  frirr  5518  wereu2  5538  tz6.26  6165  fndmdifeq0  6800  fnnfpeq0  6926  wemapso2  9003  wemapwe  9146  hashbclem  13800  hashbc  13801  wrdnfi  13885  smuval2  15814  smupvallem  15815  smu01lem  15817  smumullem  15824  phiprmpw  16096  hashgcdeq  16109  prmreclem4  16238  cshws0  16418  pmtrsn  18630  efgsfo  18848  00lsp  19736  dsmm0cl  20867  ordthauslem  21974  pthaus  22229  xkohaus  22244  hmeofval  22349  mumul  25744  musum  25754  ppiub  25766  lgsquadlem2  25943  umgrnloop0  26880  lfgrnloop  26896  numedglnl  26915  usgrnloop0ALT  26973  lfuhgr1v0e  27022  nbuhgr  27111  nbumgr  27115  uhgrnbgr0nb  27122  nbgr0vtxlem  27123  vtxd0nedgb  27256  vtxdusgr0edgnelALT  27264  1loopgrnb0  27270  usgrvd0nedg  27301  vtxdginducedm1lem4  27310  wwlks  27599  iswwlksnon  27617  iswspthsnon  27620  0enwwlksnge1  27628  wspn0  27688  rusgr0edg  27737  clwwlk  27746  clwwlkn  27789  clwwlkn0  27791  clwwlknon  27853  clwwlknon1nloop  27862  clwwlknondisj  27874  vdn0conngrumgrv2  27959  eupth2lemb  28000  eulercrct  28005  frgrregorufr0  28087  numclwwlk3lem2  28147  ofldchr  30894  measvuni  31480  dya2iocuni  31548  repr0  31889  reprlt  31897  reprgt  31899  subfacp1lem6  32439  prv1n  32685  frpomin  33085  frpomin2  33086  poimirlem26  34952  poimirlem27  34953  cnambfre  34974  itg2addnclem2  34978  areacirclem5  35018  0dioph  39467  undisjrab  40728  supminfxr  41830  dvnprodlem3  42323  pimltmnf2  43069  pimconstlt0  43072  pimgtpnf2  43075  rmsupp0  44501  lcoc0  44562  rrxsphere  44820