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

Theorem sbceq1d 3776
Description: Equality theorem for class substitution. (Contributed by Mario Carneiro, 9-Feb-2017.) (Revised by NM, 30-Jun-2018.)
Hypothesis
Ref Expression
sbceq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
sbceq1d (𝜑 → ([𝐴 / 𝑥]𝜓[𝐵 / 𝑥]𝜓))

Proof of Theorem sbceq1d
StepHypRef Expression
1 sbceq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 dfsbcq 3773 . 2 (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜓[𝐵 / 𝑥]𝜓))
31, 2syl 17 1 (𝜑 → ([𝐴 / 𝑥]𝜓[𝐵 / 𝑥]𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  [wsbc 3771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814  df-clel 2893  df-sbc 3772
This theorem is referenced by:  sbceq1dd  3777  sbcnestgfw  4369  sbcnestgf  4374  ralrnmptw  6853  ralrnmpt  6855  tfindes  7565  findes  7600  findcard2  8747  ac6sfi  8751  indexfi  8821  ac6num  9890  nn1suc  11648  uzind4s  12297  uzind4s2  12298  fzrevral  12982  fzshftral  12985  fi1uzind  13845  wrdind  14074  wrd2ind  14075  cjth  14452  prmind2  16019  isprs  17530  isdrs  17534  joinlem  17611  meetlem  17625  istos  17635  isdlat  17793  gsumvalx  17876  mndind  17982  issrg  19188  islmod  19569  quotval  24810  nn0min  30464  wrdt2ind  30555  bnj944  32110  sdclem2  34900  fdc  34903  hdmap1ffval  38813  hdmap1fval  38814  rexrabdioph  39271  2nn0ind  39422  zindbi  39423  iotasbcq  40649  prproropreud  43518
  Copyright terms: Public domain W3C validator