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

Theorem sbceq1d 3407
 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 3404 . 2 (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜓[𝐵 / 𝑥]𝜓))
31, 2syl 17 1 (𝜑 → ([𝐴 / 𝑥]𝜓[𝐵 / 𝑥]𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475  [wsbc 3402 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606  df-sbc 3403 This theorem is referenced by:  sbceq1dd  3408  sbcnestgf  3947  ralrnmpt  6276  tfindes  6954  findes  6988  findcard2  8085  ac6sfi  8089  indexfi  8157  ac6num  9184  nn1suc  10918  uzind4s  11624  uzind4s2  11625  fzrevral  12294  fzshftral  12297  fi1uzind  13134  fi1uzindOLD  13140  wrdind  13328  wrd2ind  13329  cjth  13691  prmind2  15236  isprs  16753  isdrs  16757  joinlem  16834  meetlem  16848  istos  16858  isdlat  17016  gsumvalx  17093  mrcmndind  17189  issrg  18330  islmod  18690  quotval  23851  nn0min  28954  bnj944  30262  sdclem2  32708  fdc  32711  hdmap1ffval  36103  hdmap1fval  36104  rexrabdioph  36376  2nn0ind  36528  zindbi  36529  iotasbcq  37660
 Copyright terms: Public domain W3C validator