Theorem rabeq0 3911

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 3905	. 2 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		df-rab 2905	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
3	2	eqeq1i 2615	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅)
4		raln 2974	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
5	1, 3, 4	3bitr4i 291	1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 195   ∧ wa 383  ∀wal 1473   = wceq 1475   ∈ wcel 1977  {cab 2596  ∀wral 2896  {crab 2900  ∅c0 3874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rab 2905  df-v 3175  df-dif 3543  df-nul 3875

This theorem is referenced by:  rabn0  3912  rabnc  3916  dffr2  5003  frc  5004  frirr  5015  wereu2  5035  tz6.26  5628  fndmdifeq0  6231  fnnfpeq0  6349  wemapso2  8341  wemapwe  8477  hashbclem  13093  hashbc  13094  smuval2  15042  smupvallem  15043  smu01lem  15045  smumullem  15052  phiprmpw  15319  hashgcdeq  15332  prmreclem4  15461  cshws0  15646  pmtrsn  17762  efgsfo  17975  00lsp  18802  dsmm0cl  19903  ordthauslem  20997  pthaus  21251  xkohaus  21266  hmeofval  21371  mumul  24707  musum  24717  ppiub  24729  lgsquadlem2  24906  umgrnloop0  25775  lfgrnloop  25791  usgranloop0  25909  usgra1v  25919  nbusgra  25957  nbgra0nb  25958  nbgra0edg  25961  cusgrasizeindslem1  26002  uvtx0  26019  clwwlkn0  26302  vdgr1b  26431  vdgr1a  26433  vdusgra0nedg  26435  usgravd0nedg  26445  eupath2  26507  vdn0frgrav2  26550  vdgn0frgrav2  26551  frgraregorufr0  26579  2spot0  26591  numclwwlkdisj  26607  numclwwlk3lem  26635  ofldchr  29145  measvuni  29604  dya2iocuni  29672  subfacp1lem6  30421  poimirlem26  32605  poimirlem27  32606  cnambfre  32628  itg2addnclem2  32632  areacirclem5  32674  0dioph  36360  undisjrab  37527  dvnprodlem3  38838  pimltmnf2  39588  pimconstlt0  39591  pimgtpnf2  39594  usgrnloop0ALT  40432  lfuhgr1v0e  40480  nbuhgr  40565  nbumgr  40569  uhgrnbgr0nb  40576  nbgr0vtxlem  40577  vtxd0nedgb  40703  vtxdusgr0edgnelALT  40711  1loopgrnb0  40717  usgrvd0nedg  40749  wwlks  41038  0enwwlksnge1  41060  wspn0  41131  rusgr0edg  41176  clwwlks  41187  clwwlksndisj  41280  vdn0conngrumgrv2  41363  eupth2lemb  41405  eulercrct  41410  frgrregorufr0  41489  av-numclwwlk3lem  41538  rmsupp0  41943  lcoc0  42005