Theorem csbeq2i 3929

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

Syntax hints:   = wceq 1537  ⊤wtru 1538  ⦋csb 3921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-sbc 3805  df-csb 3922

This theorem is referenced by:  csbnest1g  4455  csbvarg  4457  csbsng  4733  csbprg  4734  csbopg  4915  csbuni  4960  csbmpt12  5576  csbxp  5799  csbcnv  5908  csbcnvgALT  5909  csbdm  5922  csbres  6012  csbrn  6234  csbpredg  6338  csbfv12  6968  fvmpocurryd  8312  csbfrecsg  8325  csbwrecsg  8362  csbnegg  11533  csbwrdg  14592  matgsum  22464  precsexlemcbv  28248  precsexlem3  28251  disjxpin  32610  f1od2  32735  sumeq2si  36166  prodeq2si  36168  bj-csbsn  36870  csbrecsg  37294  csbrdgg  37295  csboprabg  37296  csbmpo123  37297  csbfinxpg  37354  poimirlem24  37604  cdleme31so  40336  cdleme31sn  40337  cdleme31sn1  40338  cdleme31se  40339  cdleme31se2  40340  cdleme31sc  40341  cdleme31sde  40342  cdleme31sn2  40346  cdlemkid3N  40890  cdlemkid4  40891  climinf2mpt  45635  climinfmpt  45636