MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rabeq0 Structured version   Visualization version   GIF version

Theorem rabeq0 3948
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
StepHypRef Expression
1 ab0 3942 . 2 ({𝑥 ∣ (𝑥𝐴𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥𝐴𝜑))
2 df-rab 2918 . . 3 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
32eqeq1i 2625 . 2 ({𝑥𝐴𝜑} = ∅ ↔ {𝑥 ∣ (𝑥𝐴𝜑)} = ∅)
4 raln 2988 . 2 (∀𝑥𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥𝐴𝜑))
51, 3, 43bitr4i 292 1 ({𝑥𝐴𝜑} = ∅ ↔ ∀𝑥𝐴 ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wa 384  wal 1479   = wceq 1481  wcel 1988  {cab 2606  wral 2909  {crab 2913  c0 3907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rab 2918  df-v 3197  df-dif 3570  df-nul 3908
This theorem is referenced by:  rabn0  3949  rabnc  3953  dffr2  5069  frc  5070  frirr  5081  wereu2  5101  tz6.26  5699  fndmdifeq0  6309  fnnfpeq0  6429  wemapso2  8443  wemapwe  8579  hashbclem  13219  hashbc  13220  smuval2  15185  smupvallem  15186  smu01lem  15188  smumullem  15195  phiprmpw  15462  hashgcdeq  15475  prmreclem4  15604  cshws0  15789  pmtrsn  17920  efgsfo  18133  00lsp  18962  dsmm0cl  20065  ordthauslem  21168  pthaus  21422  xkohaus  21437  hmeofval  21542  mumul  24888  musum  24898  ppiub  24910  lgsquadlem2  25087  umgrnloop0  25985  lfgrnloop  26001  numedglnl  26020  usgrnloop0ALT  26078  lfuhgr1v0e  26127  nbuhgr  26220  nbumgr  26224  uhgrnbgr0nb  26231  nbgr0vtxlem  26232  vtxd0nedgb  26365  vtxdusgr0edgnelALT  26373  1loopgrnb0  26379  usgrvd0nedg  26410  vtxdginducedm1lem4  26419  wwlks  26708  0enwwlksnge1  26730  wspn0  26801  rusgr0edg  26849  clwwlks  26860  clwwlksndisj  26953  vdn0conngrumgrv2  27036  eupth2lemb  27077  eulercrct  27082  frgrregorufr0  27162  numclwwlk3lem  27212  ofldchr  29788  measvuni  30251  dya2iocuni  30319  repr0  30663  reprlt  30671  reprgt  30673  subfacp1lem6  31141  poimirlem26  33406  poimirlem27  33407  cnambfre  33429  itg2addnclem2  33433  areacirclem5  33475  0dioph  37161  undisjrab  38325  supminfxr  39507  dvnprodlem3  39926  pimltmnf2  40674  pimconstlt0  40677  pimgtpnf2  40680  rmsupp0  41914  lcoc0  41976
  Copyright terms: Public domain W3C validator