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 3419	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
3	2	eqeq1i 2770	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅)
4		raln 3090	. 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 2146  {cab 2743  ∀wral 3081  {crab 3418  ∅c0 4286

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 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2744  df-cleq 2757  df-ral 3082  df-rab 3419  df-dif 3909  df-nul 4287

This theorem is used by:  rabn0  4346  rabnc  4348  dffr2ALT  5625  wereu2  5660  frpomin  6345  frpomin2  6346  fndmdifeq0  7043  fnnfpeq0  7182  wemapso2  9522  wemapwe  9673  hashbclem  14507  hashbc  14508  wrdnfi  14603  smuval2  16562  smupvallem  16563  smu01lem  16565  smumullem  16572  phiprmpw  16857  hashgcdeq  16871  prmreclem4  17001  cshws0  17183  pmtrsn  19633  efgsfo  19853  00lsp  21152  ofldchr  21776  dsmm0cl  21940  ordthauslem  23590  pthaus  23846  xkohaus  23861  hmeofval  23966  mumul  27396  musum  27406  ppiub  27419  lgsquadlem2  27596  umgrnloop0  29514  lfgrnloop  29530  numedglnl  29549  usgrnloop0ALT  29613  lfuhgr1v0e  29662  nbuhgr  29751  nbumgr  29755  uhgrnbgr0nb  29762  nbgr0edglem  29764  vtxd0nedgb  29896  vtxdusgr0edgnelALT  29904  1loopgrnb0  29910  usgrvd0nedg  29941  vtxdginducedm1lem4  29950  wwlks  30251  iswwlksnon  30269  iswspthsnon  30272  0enwwlksnge1  30280  wspn0  30340  rusgr0edg  30392  clwwlk  30401  clwwlkn  30444  clwwlkn0  30446  clwwlknon  30508  clwwlknon1nloop  30517  clwwlknondisj  30529  vdn0conngrumgrv2  30618  eupth2lemb  30659  eulercrct  30664  frgrregorufr0  30746  numclwwlk3lem2  30806  esplyfval2  34019  2sqr3minply  34234  cos9thpiminply  34242  zarcls1  34323  measvuni  34669  dya2iocuni  34738  repr0  35063  reprlt  35071  reprgt  35073  nummin  35542  fineqvnttrclselem1  35591  subfacp1lem6  35714  prv1n  35960  poimirlem26  38354  poimirlem27  38355  cnambfre  38376  itg2addnclem2  38380  areacirclem5  38420  sticksstones1  42971  nna4b4nsq  43450  0dioph  43567  undisjrab  45074  supminfxr  46236  dvnprodlem3  46720  pimltmnf2f  47469  pimconstlt0  47473  pimgtpnf2f  47477  isubgr0uhgr  48696  stgr0  48783  rmsupp0  49205  lcoc0  49259  rrxsphere  49585