Theorem csbeq2i 3858

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

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

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-sbc 3742  df-csb 3851

This theorem is referenced by:  csbnest1g  4382  csbvarg  4384  csbsng  4661  csbprg  4662  csbopg  4843  csbuni  4888  csbmpt12  5497  csbxp  5716  csbcnv  5823  csbcnvgALT  5824  csbdm  5837  csbres  5931  csbrn  6150  csbpredg  6254  csbfv12  6867  fvmpocurryd  8201  csbfrecsg  8214  csbwrecsg  8248  csbnegg  11354  csbwrdg  14448  matgsum  22350  precsexlemcbv  28142  precsexlem3  28145  disjxpin  32563  f1od2  32697  sumeq2si  36235  prodeq2si  36237  bj-csbsn  36937  csbrecsg  37361  csbrdgg  37362  csboprabg  37363  csbmpo123  37364  csbfinxpg  37421  poimirlem24  37683  cdleme31so  40417  cdleme31sn  40418  cdleme31sn1  40419  cdleme31se  40420  cdleme31se2  40421  cdleme31sc  40422  cdleme31sde  40423  cdleme31sn2  40427  cdlemkid3N  40971  cdlemkid4  40972  climinf2mpt  45751  climinfmpt  45752