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

Theorem csbeq2i 3890
 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 3889 . 2 (⊤ → 𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶)
43mptru 1540 1 𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶
 Colors of variables: wff setvar class Syntax hints:   = wceq 1533  ⊤wtru 1534  ⦋csb 3882 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-12 2173  ax-ext 2793 This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-sbc 3772  df-csb 3883 This theorem is referenced by:  csbnest1g  4380  csbvarg  4382  csbsng  4637  csbprg  4638  csbopg  4814  csbuni  4859  csbmpt12  5436  csbxp  5644  csbcnv  5748  csbcnvgALT  5749  csbdm  5760  csbres  5850  csbrn  6054  csbfv12  6707  fvmpocurryd  7931  csbnegg  10877  csbwrdg  13889  matgsum  21040  disjxpin  30332  f1od2  30451  bj-csbsn  34216  csbpredg  34601  csbwrecsg  34602  csbrecsg  34603  csbrdgg  34604  csboprabg  34605  csbmpo123  34606  csbfinxpg  34663  poimirlem24  34910  cdleme31so  37509  cdleme31sn  37510  cdleme31sn1  37511  cdleme31se  37512  cdleme31se2  37513  cdleme31sc  37514  cdleme31sde  37515  cdleme31sn2  37519  cdlemkid3N  38063  cdlemkid4  38064  climinf2mpt  41988  climinfmpt  41989
 Copyright terms: Public domain W3C validator