Theorem rabeq0 4316

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 4308	. 2 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		df-rab 3392	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
3	2	eqeq1i 2744	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅)
4		raln 3062	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
5	1, 3, 4	3bitr4i 304	1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 207   ∧ wa 396  ∀wal 1545   = wceq 1547   ∈ wcel 2119  {cab 2717  ∀wral 3053  {crab 3391  ∅c0 4261

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2718  df-cleq 2731  df-ral 3054  df-rab 3392  df-dif 3886  df-nul 4262

This theorem is referenced by:  rabn0  4317  rabnc  4319  dffr2ALT  5580  wereu2  5615  frpomin  6291  frpomin2  6292  fndmdifeq0  6985  fnnfpeq0  7122  wemapso2  9458  wemapwe  9609  hashbclem  14405  hashbc  14406  wrdnfi  14501  smuval2  16442  smupvallem  16443  smu01lem  16445  smumullem  16452  phiprmpw  16737  hashgcdeq  16751  prmreclem4  16881  cshws0  17063  pmtrsn  19485  efgsfo  19705  00lsp  20971  ofldchr  21551  dsmm0cl  21715  ordthauslem  23366  pthaus  23621  xkohaus  23636  hmeofval  23741  mumul  27162  musum  27172  ppiub  27185  lgsquadlem2  27362  umgrnloop0  29196  lfgrnloop  29212  numedglnl  29231  usgrnloop0ALT  29292  lfuhgr1v0e  29341  nbuhgr  29430  nbumgr  29434  uhgrnbgr0nb  29441  nbgr0edglem  29443  vtxd0nedgb  29575  vtxdusgr0edgnelALT  29583  1loopgrnb0  29589  usgrvd0nedg  29620  vtxdginducedm1lem4  29629  wwlks  29921  iswwlksnon  29939  iswspthsnon  29942  0enwwlksnge1  29950  wspn0  30010  rusgr0edg  30062  clwwlk  30071  clwwlkn  30114  clwwlkn0  30116  clwwlknon  30178  clwwlknon1nloop  30187  clwwlknondisj  30199  vdn0conngrumgrv2  30284  eupth2lemb  30325  eulercrct  30330  frgrregorufr0  30412  numclwwlk3lem2  30472  esplyfval2  33749  2sqr3minply  33964  cos9thpiminply  33972  zarcls1  34053  measvuni  34398  dya2iocuni  34467  repr0  34795  reprlt  34803  reprgt  34805  nummin  35274  fineqvnttrclselem1  35302  subfacp1lem6  35413  prv1n  35659  poimirlem26  38013  poimirlem27  38014  cnambfre  38035  itg2addnclem2  38039  areacirclem5  38079  sticksstones1  42631  nna4b4nsq  43110  0dioph  43227  undisjrab  44750  supminfxr  45907  dvnprodlem3  46391  pimltmnf2f  47140  pimconstlt0  47144  pimgtpnf2f  47148  isubgr0uhgr  48364  stgr0  48451  rmsupp0  48859  lcoc0  48913  rrxsphere  49239