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

Theorem rabeq0 4157
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 4152 . 2 ({𝑥 ∣ (𝑥𝐴𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥𝐴𝜑))
2 df-rab 3105 . . 3 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
32eqeq1i 2811 . 2 ({𝑥𝐴𝜑} = ∅ ↔ {𝑥 ∣ (𝑥𝐴𝜑)} = ∅)
4 raln 3179 . 2 (∀𝑥𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥𝐴𝜑))
51, 3, 43bitr4i 294 1 ({𝑥𝐴𝜑} = ∅ ↔ ∀𝑥𝐴 ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 197  wa 384  wal 1635   = wceq 1637  wcel 2156  {cab 2792  wral 3096  {crab 3100  c0 4116
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ral 3101  df-rab 3105  df-v 3393  df-dif 3772  df-nul 4117
This theorem is referenced by:  rabn0  4158  rabnc  4160  dffr2  5276  frc  5277  frirr  5288  wereu2  5308  tz6.26  5924  fndmdifeq0  6545  fnnfpeq0  6669  wemapso2  8697  wemapwe  8841  hashbclem  13453  hashbc  13454  smuval2  15423  smupvallem  15424  smu01lem  15426  smumullem  15433  phiprmpw  15698  hashgcdeq  15711  prmreclem4  15840  cshws0  16020  pmtrsn  18140  efgsfo  18353  00lsp  19188  dsmm0cl  20294  ordthauslem  21401  pthaus  21655  xkohaus  21670  hmeofval  21775  mumul  25121  musum  25131  ppiub  25143  lgsquadlem2  25320  umgrnloop0  26218  lfgrnloop  26234  numedglnl  26254  usgrnloop0ALT  26312  lfuhgr1v0e  26362  nbuhgr  26455  nbumgr  26459  uhgrnbgr0nb  26466  nbgr0vtxlem  26467  vtxd0nedgb  26612  vtxdusgr0edgnelALT  26620  1loopgrnb0  26626  usgrvd0nedg  26657  vtxdginducedm1lem4  26666  wwlks  26956  iswwlksnon  26975  iswspthsnon  26979  0enwwlksnge1  26991  wspn0  27064  rusgr0edg  27115  clwwlk  27126  clwwlkn  27171  clwwlkn0  27175  clwwlknon  27255  clwwlknon1nloop  27267  clwwlknondisj  27280  clwwlknondisjOLD  27285  vdn0conngrumgrv2  27369  eupth2lemb  27410  eulercrct  27415  frgrregorufr0  27499  numclwwlk3lemOLD  27569  numclwwlk3lem2  27572  ofldchr  30139  measvuni  30602  dya2iocuni  30670  repr0  31014  reprlt  31022  reprgt  31024  subfacp1lem6  31490  frpomin  32059  frpomin2  32060  poimirlem26  33748  poimirlem27  33749  cnambfre  33770  itg2addnclem2  33774  areacirclem5  33816  0dioph  37844  undisjrab  39005  supminfxr  40173  dvnprodlem3  40643  pimltmnf2  41393  pimconstlt0  41396  pimgtpnf2  41399  rmsupp0  42717  lcoc0  42779
  Copyright terms: Public domain W3C validator