Theorem rabeq0 4345

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

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 400  ∀wal 1568   = wceq 1570   ∈ wcel 2143  {cab 2741  ∀wral 3079  {crab 3416  ∅c0 4286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-ral 3080  df-rab 3417  df-dif 3908  df-nul 4287

This theorem is referenced by:  rabn0  4346  rabnc  4348  dffr2ALT  5623  wereu2  5658  frpomin  6341  frpomin2  6342  fndmdifeq0  7039  fnnfpeq0  7176  wemapso2  9511  wemapwe  9662  hashbclem  14485  hashbc  14486  wrdnfi  14581  smuval2  16535  smupvallem  16536  smu01lem  16538  smumullem  16545  phiprmpw  16830  hashgcdeq  16844  prmreclem4  16974  cshws0  17156  pmtrsn  19584  efgsfo  19804  00lsp  21102  ofldchr  21726  dsmm0cl  21890  ordthauslem  23540  pthaus  23795  xkohaus  23810  hmeofval  23915  mumul  27345  musum  27355  ppiub  27368  lgsquadlem2  27545  umgrnloop0  29459  lfgrnloop  29475  numedglnl  29494  usgrnloop0ALT  29555  lfuhgr1v0e  29604  nbuhgr  29693  nbumgr  29697  uhgrnbgr0nb  29704  nbgr0edglem  29706  vtxd0nedgb  29838  vtxdusgr0edgnelALT  29846  1loopgrnb0  29852  usgrvd0nedg  29883  vtxdginducedm1lem4  29892  wwlks  30184  iswwlksnon  30202  iswspthsnon  30205  0enwwlksnge1  30213  wspn0  30273  rusgr0edg  30325  clwwlk  30334  clwwlkn  30377  clwwlkn0  30379  clwwlknon  30441  clwwlknon1nloop  30450  clwwlknondisj  30462  vdn0conngrumgrv2  30547  eupth2lemb  30588  eulercrct  30593  frgrregorufr0  30675  numclwwlk3lem2  30735  esplyfval2  33955  2sqr3minply  34170  cos9thpiminply  34178  zarcls1  34259  measvuni  34604  dya2iocuni  34673  repr0  34998  reprlt  35006  reprgt  35008  nummin  35484  fineqvnttrclselem1  35534  subfacp1lem6  35677  prv1n  35923  poimirlem26  38297  poimirlem27  38298  cnambfre  38319  itg2addnclem2  38323  areacirclem5  38363  sticksstones1  42913  nna4b4nsq  43392  0dioph  43509  undisjrab  45016  supminfxr  46178  dvnprodlem3  46662  pimltmnf2f  47411  pimconstlt0  47415  pimgtpnf2f  47419  isubgr0uhgr  48638  stgr0  48725  rmsupp0  49148  lcoc0  49202  rrxsphere  49528