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

Theorem rabeq0 3907
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 3901 . 2 ({𝑥 ∣ (𝑥𝐴𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥𝐴𝜑))
2 df-rab 2901 . . 3 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
32eqeq1i 2611 . 2 ({𝑥𝐴𝜑} = ∅ ↔ {𝑥 ∣ (𝑥𝐴𝜑)} = ∅)
4 raln 2970 . 2 (∀𝑥𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥𝐴𝜑))
51, 3, 43bitr4i 290 1 ({𝑥𝐴𝜑} = ∅ ↔ ∀𝑥𝐴 ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 194  wa 382  wal 1472   = wceq 1474  wcel 1976  {cab 2592  wral 2892  {crab 2896  c0 3870
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ral 2897  df-rab 2901  df-v 3171  df-dif 3539  df-nul 3871
This theorem is referenced by:  rabn0  3908  rabnc  3912  dffr2  4990  frc  4991  frirr  5002  wereu2  5022  tz6.26  5611  fndmdifeq0  6213  fnnfpeq0  6324  wemapso2  8315  wemapwe  8451  hashbclem  13042  hashbc  13043  smuval2  14985  smupvallem  14986  smu01lem  14988  smumullem  14995  phiprmpw  15262  hashgcdeq  15275  prmreclem4  15404  cshws0  15589  pmtrsn  17705  efgsfo  17918  00lsp  18745  dsmm0cl  19842  ordthauslem  20936  pthaus  21190  xkohaus  21205  hmeofval  21310  mumul  24621  musum  24631  ppiub  24643  lgsquadlem2  24820  usgranloop0  25672  usgra1v  25682  nbusgra  25720  nbgra0nb  25721  nbgra0edg  25724  cusgrasizeindslem1  25765  uvtx0  25782  clwwlkn0  26065  vdgr1b  26194  vdgr1a  26196  vdusgra0nedg  26198  usgravd0nedg  26208  eupath2  26270  vdn0frgrav2  26313  vdgn0frgrav2  26314  frgraregorufr0  26342  2spot0  26354  numclwwlkdisj  26370  numclwwlk3lem  26398  ofldchr  28948  measvuni  29407  dya2iocuni  29475  subfacp1lem6  30224  poimirlem26  32405  poimirlem27  32406  cnambfre  32428  itg2addnclem2  32432  areacirclem5  32474  0dioph  36160  undisjrab  37327  dvnprodlem3  38639  pimltmnf2  39389  pimconstlt0  39392  pimgtpnf2  39395  umgrnloop0  40333  lfgrnloop  40349  usgrnloop0ALT  40431  lfuhgr1v0e  40479  nbuhgr  40564  nbumgr  40568  uhgrnbgr0nb  40575  nbgr0vtxlem  40576  vtxd0nedgb  40702  vtxdusgr0edgnelALT  40710  1loopgrnb0  40716  usgrvd0nedg  40748  wwlks  41037  0enwwlksnge1  41059  wspn0  41130  rusgr0edg  41175  clwwlks  41186  clwwlksndisj  41279  vdn0conngrumgrv2  41362  eupth2lemb  41404  eulercrct  41409  frgrregorufr0  41488  av-numclwwlk3lem  41537  rmsupp0  41942  lcoc0  42004
  Copyright terms: Public domain W3C validator