Theorem csbeq2i 3846

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-sbc 3730  df-csb 3839

This theorem is referenced by:  csbnest1g  4373  csbvarg  4375  csbsng  4653  csbprg  4654  csbopg  4835  csbuni  4881  csbmpt12  5505  csbxp  5725  csbcnv  5832  csbcnvgALT  5833  csbdm  5846  csbres  5941  csbrn  6161  csbpredg  6265  csbfv12  6879  fvmpocurryd  8214  csbfrecsg  8227  csbwrecsg  8261  csbnegg  11381  csbwrdg  14497  matgsum  22412  precsexlemcbv  28212  precsexlem3  28215  disjxpin  32673  f1od2  32807  sumeq2si  36400  prodeq2si  36402  bj-csbsn  37227  csbrecsg  37658  csbrdgg  37659  csboprabg  37660  csbmpo123  37661  csbfinxpg  37718  poimirlem24  37979  cdleme31so  40839  cdleme31sn  40840  cdleme31sn1  40841  cdleme31se  40842  cdleme31se2  40843  cdleme31sc  40844  cdleme31sde  40845  cdleme31sn2  40849  cdlemkid3N  41393  cdlemkid4  41394  climinf2mpt  46160  climinfmpt  46161