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 1554	1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶

Syntax hints:   = wceq 1547  ⊤wtru 1548  ⦋csb 3838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-sbc 3731  df-csb 3839

This theorem is referenced by:  csbnest1g  4367  csbvarg  4369  csbsng  4647  csbprg  4648  csbopg  4829  csbuni  4875  csbmpt12  5506  csbxp  5726  csbcnv  5832  csbcnvgALT  5833  csbdm  5846  csbres  5941  csbrn  6161  csbpredg  6265  csbfv12  6879  fvmpocurryd  8218  csbfrecsg  8231  csbwrecsg  8265  csbnegg  11388  csbwrdg  14504  matgsum  22427  precsexlemcbv  28223  precsexlem3  28226  disjxpin  32684  f1od2  32818  sumeq2si  36437  prodeq2si  36439  bj-csbsn  37264  csbrecsg  37697  csbrdgg  37698  csboprabg  37699  csbmpo123  37700  csbfinxpg  37757  poimirlem24  38018  cdleme31so  40878  cdleme31sn  40879  cdleme31sn1  40880  cdleme31se  40881  cdleme31se2  40882  cdleme31sc  40883  cdleme31sde  40884  cdleme31sn2  40888  cdlemkid3N  41432  cdlemkid4  41433  climinf2mpt  46164  climinfmpt  46165