Theorem rabeq0 4341

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570   ∈ wcel 2147  {cab 2741  ∀wral 3080  {crab 3416  ∅c0 4281

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-clab 2742  df-cleq 2755  df-ral 3081  df-rab 3417  df-dif 4050  df-nul 4282

This theorem is used by:  rabn0  4342  rabnc  4344  dffr2ALT  5620  wereu2  5655  frpomin  6369  frpomin2  6370  fndmdifeq0  7074  fnnfpeq0  7214  wemapso2  9584  wemapwe  9735  hashbclem  14638  hashbc  14639  wrdnfi  14734  smuval2  16696  smupvallem  16697  smu01lem  16699  smumullem  16706  phiprmpw  16997  hashgcdeq  17011  prmreclem4  17141  cshws0  17323  pmtrsn  19784  efgsfo  20004  00lsp  21307  ofldchr  21937  dsmm0cl  22101  ordthauslem  23756  pthaus  24012  xkohaus  24027  hmeofval  24132  mumul  27565  musum  27575  ppiub  27588  lgsquadlem2  27765  nna4b4nsq  28047  umgrnloop0  29744  lfgrnloop  29760  numedglnl  29779  usgrnloop0ALT  29843  lfuhgr1v0e  29892  nbuhgr  29981  nbumgr  29985  uhgrnbgr0nb  29992  nbgr0edglem  29994  vtxd0nedgb  30126  vtxdusgr0edgnelALT  30134  1loopgrnb0  30140  usgrvd0nedg  30171  vtxdginducedm1lem4  30180  wwlks  30481  iswwlksnon  30499  iswspthsnon  30502  0enwwlksnge1  30510  wspn0  30570  rusgr0edg  30622  clwwlk  30631  clwwlkn  30674  clwwlkn0  30676  clwwlknon  30738  clwwlknon1nloop  30747  clwwlknondisj  30759  vdn0conngrumgrv2  30854  eupth2lemb  30895  eulercrct  30900  frgrregorufr0  30982  numclwwlk3lem2  31042  esplyfval2  34308  2sqr3minply  34523  cos9thpiminply  34531  zarcls1  34612  measvuni  34958  dya2iocuni  35026  repr0  35351  reprlt  35359  reprgt  35361  nummin  35847  fineqvnttrclselem1  35930  subfacp1lem6  36158  prv1n  36404  poimirlem26  38832  poimirlem27  38833  cnambfre  38854  itg2addnclem2  38858  areacirclem5  38898  sticksstones1  43462  frlmnzcoordex  43918  0dioph  44055  undisjrab  45551  supminfxr  46747  dvnprodlem3  47231  pimltmnf2f  47980  pimconstlt0  47984  pimgtpnf2f  47988  isubgr0uhgr  49244  stgr0  49331  rmsupp0  49811  lcoc0  49865  rrxsphere  50191