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

Theorem sbceq1d 3711
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 3708 . 2 (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜓[𝐵 / 𝑥]𝜓))
31, 2syl 17 1 (𝜑 → ([𝐴 / 𝑥]𝜓[𝐵 / 𝑥]𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1522  [wsbc 3706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-ext 2769
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-cleq 2788  df-clel 2863  df-sbc 3707
This theorem is referenced by:  sbceq1dd  3712  sbcnestgf  4290  ralrnmpt  6725  tfindes  7433  findes  7468  findcard2  8604  ac6sfi  8608  indexfi  8678  ac6num  9747  nn1suc  11507  uzind4s  12157  uzind4s2  12158  fzrevral  12842  fzshftral  12845  fi1uzind  13701  wrdind  13920  wrd2ind  13921  cjth  14296  prmind2  15858  isprs  17369  isdrs  17373  joinlem  17450  meetlem  17464  istos  17474  isdlat  17632  gsumvalx  17709  mndind  17805  issrg  18947  islmod  19328  quotval  24564  nn0min  30221  wrdt2ind  30306  bnj944  31826  sdclem2  34549  fdc  34552  hdmap1ffval  38462  hdmap1fval  38463  rexrabdioph  38876  2nn0ind  39027  zindbi  39028  iotasbcq  40307  prproropreud  43153
  Copyright terms: Public domain W3C validator