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

Theorem csbeq2i 3907
Description: Formula-building inference for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
Hypothesis
Ref Expression
csbeq2i.1 𝐵 = 𝐶
Assertion
Ref Expression
csbeq2i 𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶

Proof of Theorem csbeq2i
StepHypRef Expression
1 csbeq2i.1 . . . 4 𝐵 = 𝐶
21a1i 11 . . 3 (⊤ → 𝐵 = 𝐶)
32csbeq2dv 3906 . 2 (⊤ → 𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶)
43mptru 1547 1 𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  wtru 1541  csb 3899
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-sbc 3789  df-csb 3900
This theorem is referenced by:  csbnest1g  4432  csbvarg  4434  csbsng  4708  csbprg  4709  csbopg  4891  csbuni  4936  csbmpt12  5562  csbxp  5785  csbcnv  5894  csbcnvgALT  5895  csbdm  5908  csbres  6000  csbrn  6223  csbpredg  6327  csbfv12  6954  fvmpocurryd  8296  csbfrecsg  8309  csbwrecsg  8346  csbnegg  11505  csbwrdg  14582  matgsum  22443  precsexlemcbv  28230  precsexlem3  28233  disjxpin  32601  f1od2  32732  sumeq2si  36203  prodeq2si  36205  bj-csbsn  36905  csbrecsg  37329  csbrdgg  37330  csboprabg  37331  csbmpo123  37332  csbfinxpg  37389  poimirlem24  37651  cdleme31so  40381  cdleme31sn  40382  cdleme31sn1  40383  cdleme31se  40384  cdleme31se2  40385  cdleme31sc  40386  cdleme31sde  40387  cdleme31sn2  40391  cdlemkid3N  40935  cdlemkid4  40936  climinf2mpt  45729  climinfmpt  45730
  Copyright terms: Public domain W3C validator