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 4330	. 2 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		df-rab 3398	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
3	2	eqeq1i 2739	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅)
4		raln 3057	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
5	1, 3, 4	3bitr4i 303	1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395  ∀wal 1539   = wceq 1541   ∈ wcel 2113  {cab 2712  ∀wral 3049  {crab 3397  ∅c0 4283

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 1968  ax-7 2009  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2713  df-cleq 2726  df-ral 3050  df-rab 3398  df-dif 3902  df-nul 4284

This theorem is referenced by:  rabn0  4339  rabnc  4341  dffr2ALT  5584  wereu2  5619  frpomin  6296  frpomin2  6297  fndmdifeq0  6987  fnnfpeq0  7122  wemapso2  9456  wemapwe  9604  hashbclem  14373  hashbc  14374  wrdnfi  14469  smuval2  16407  smupvallem  16408  smu01lem  16410  smumullem  16417  phiprmpw  16701  hashgcdeq  16715  prmreclem4  16845  cshws0  17027  pmtrsn  19446  efgsfo  19666  00lsp  20930  ofldchr  21529  dsmm0cl  21693  ordthauslem  23325  pthaus  23580  xkohaus  23595  hmeofval  23700  mumul  27145  musum  27155  ppiub  27169  lgsquadlem2  27346  umgrnloop0  29131  lfgrnloop  29147  numedglnl  29166  usgrnloop0ALT  29227  lfuhgr1v0e  29276  nbuhgr  29365  nbumgr  29369  uhgrnbgr0nb  29376  nbgr0edglem  29378  vtxd0nedgb  29511  vtxdusgr0edgnelALT  29519  1loopgrnb0  29525  usgrvd0nedg  29556  vtxdginducedm1lem4  29565  wwlks  29857  iswwlksnon  29875  iswspthsnon  29878  0enwwlksnge1  29886  wspn0  29946  rusgr0edg  29998  clwwlk  30007  clwwlkn  30050  clwwlkn0  30052  clwwlknon  30114  clwwlknon1nloop  30123  clwwlknondisj  30135  vdn0conngrumgrv2  30220  eupth2lemb  30261  eulercrct  30266  frgrregorufr0  30348  numclwwlk3lem2  30408  esplyfval2  33672  2sqr3minply  33886  cos9thpiminply  33894  zarcls1  33975  measvuni  34320  dya2iocuni  34389  repr0  34717  reprlt  34725  reprgt  34727  nummin  35198  fineqvnttrclselem1  35226  subfacp1lem6  35328  prv1n  35574  poimirlem26  37786  poimirlem27  37787  cnambfre  37808  itg2addnclem2  37812  areacirclem5  37852  sticksstones1  42339  nna4b4nsq  42845  0dioph  42962  undisjrab  44489  supminfxr  45650  dvnprodlem3  46134  pimltmnf2f  46883  pimconstlt0  46887  pimgtpnf2f  46891  isubgr0uhgr  48061  stgr0  48148  rmsupp0  48556  lcoc0  48610  rrxsphere  48936