Theorem csbeq2i 3845

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

Step	Hyp	Ref	Expression
1		csbeq2i.1	. . . 4 ⊢ 𝐵 = 𝐶
2	1	a1i 11	. . 3 ⊢ (⊤ → 𝐵 = 𝐶)
3	2	csbeq2dv 3844	. 2 ⊢ (⊤ → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)
4	3	mptru 1549	1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶

Syntax hints:   = wceq 1542  ⊤wtru 1543  ⦋csb 3837

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-sbc 3729  df-csb 3838

This theorem is referenced by:  csbnest1g  4372  csbvarg  4374  csbsng  4652  csbprg  4653  csbopg  4834  csbuni  4880  csbmpt12  5512  csbxp  5732  csbcnv  5838  csbcnvgALT  5839  csbdm  5852  csbres  5947  csbrn  6167  csbpredg  6271  csbfv12  6885  fvmpocurryd  8221  csbfrecsg  8234  csbwrecsg  8268  csbnegg  11390  csbwrdg  14506  matgsum  22402  precsexlemcbv  28198  precsexlem3  28201  disjxpin  32658  f1od2  32792  sumeq2si  36384  prodeq2si  36386  bj-csbsn  37211  csbrecsg  37644  csbrdgg  37645  csboprabg  37646  csbmpo123  37647  csbfinxpg  37704  poimirlem24  37965  cdleme31so  40825  cdleme31sn  40826  cdleme31sn1  40827  cdleme31se  40828  cdleme31se2  40829  cdleme31sc  40830  cdleme31sde  40831  cdleme31sn2  40835  cdlemkid3N  41379  cdlemkid4  41380  climinf2mpt  46142  climinfmpt  46143