Theorem csbeq2i 3854

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 3853	. 2 ⊢ (⊤ → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)
4	3	mptru 1548	1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶

Syntax hints:   = wceq 1541  ⊤wtru 1542  ⦋csb 3846

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-sbc 3738  df-csb 3847

This theorem is referenced by:  csbnest1g  4381  csbvarg  4383  csbsng  4660  csbprg  4661  csbopg  4842  csbuni  4888  csbmpt12  5500  csbxp  5720  csbcnv  5827  csbcnvgALT  5828  csbdm  5841  csbres  5935  csbrn  6155  csbpredg  6259  csbfv12  6873  fvmpocurryd  8207  csbfrecsg  8220  csbwrecsg  8254  csbnegg  11364  csbwrdg  14453  matgsum  22353  precsexlemcbv  28145  precsexlem3  28148  disjxpin  32570  f1od2  32706  sumeq2si  36267  prodeq2si  36269  bj-csbsn  36969  csbrecsg  37393  csbrdgg  37394  csboprabg  37395  csbmpo123  37396  csbfinxpg  37453  poimirlem24  37704  cdleme31so  40498  cdleme31sn  40499  cdleme31sn1  40500  cdleme31se  40501  cdleme31se2  40502  cdleme31sc  40503  cdleme31sde  40504  cdleme31sn2  40508  cdlemkid3N  41052  cdlemkid4  41053  climinf2mpt  45836  climinfmpt  45837