Theorem rabeq0 4338

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 4329	. 2 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		df-rab 3413	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
3	2	eqeq1i 2765	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅)
4		raln 3085	. 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 2145  {cab 2738  ∀wral 3076  {crab 3412  ∅c0 4279

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 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

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 2739  df-cleq 2752  df-ral 3077  df-rab 3413  df-dif 3902  df-nul 4280

This theorem is used by:  rabn0  4339  rabnc  4341  dffr2ALT  5617  wereu2  5652  frpomin  6338  frpomin2  6339  fndmdifeq0  7036  fnnfpeq0  7176  wemapso2  9525  wemapwe  9676  hashbclem  14517  hashbc  14518  wrdnfi  14613  smuval2  16572  smupvallem  16573  smu01lem  16575  smumullem  16582  phiprmpw  16867  hashgcdeq  16881  prmreclem4  17011  cshws0  17193  pmtrsn  19646  efgsfo  19866  00lsp  21165  ofldchr  21789  dsmm0cl  21953  ordthauslem  23608  pthaus  23864  xkohaus  23879  hmeofval  23984  mumul  27417  musum  27427  ppiub  27440  lgsquadlem2  27617  umgrnloop0  29566  lfgrnloop  29582  numedglnl  29601  usgrnloop0ALT  29665  lfuhgr1v0e  29714  nbuhgr  29803  nbumgr  29807  uhgrnbgr0nb  29814  nbgr0edglem  29816  vtxd0nedgb  29948  vtxdusgr0edgnelALT  29956  1loopgrnb0  29962  usgrvd0nedg  29993  vtxdginducedm1lem4  30002  wwlks  30303  iswwlksnon  30321  iswspthsnon  30324  0enwwlksnge1  30332  wspn0  30392  rusgr0edg  30444  clwwlk  30453  clwwlkn  30496  clwwlkn0  30498  clwwlknon  30560  clwwlknon1nloop  30569  clwwlknondisj  30581  vdn0conngrumgrv2  30676  eupth2lemb  30717  eulercrct  30722  frgrregorufr0  30804  numclwwlk3lem2  30864  esplyfval2  34075  2sqr3minply  34290  cos9thpiminply  34298  zarcls1  34379  measvuni  34725  dya2iocuni  34794  repr0  35119  reprlt  35127  reprgt  35129  nummin  35598  fineqvnttrclselem1  35647  subfacp1lem6  35764  prv1n  36010  poimirlem26  38395  poimirlem27  38396  cnambfre  38417  itg2addnclem2  38421  areacirclem5  38461  sticksstones1  43012  nna4b4nsq  43506  0dioph  43623  undisjrab  45130  supminfxr  46292  dvnprodlem3  46776  pimltmnf2f  47525  pimconstlt0  47529  pimgtpnf2f  47533  isubgr0uhgr  48789  stgr0  48876  rmsupp0  49298  lcoc0  49352  rrxsphere  49678