Theorem csbeq2i 3860

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

Syntax hints:   = wceq 1559  ⊤wtru 1560  ⦋csb 3852

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-sbc 3745  df-csb 3853

This theorem is referenced by:  csbnest1g  4385  csbvarg  4387  csbsng  4666  csbprg  4667  csbopg  4848  csbuni  4895  csbmpt12  5526  csbxp  5746  csbcnv  5856  csbcnvOLD  5857  csbcnvgALTOLD  5858  csbdm  5871  csbres  5966  csbrn  6186  csbpredg  6290  csbfv12  6908  fvmpocurryd  8246  csbfrecsg  8260  csbwrecsg  8294  csbnegg  11424  csbwrdg  14554  matgsum  22477  precsexlemcbv  28276  precsexlem3  28279  disjxpin  32737  f1od2  32871  sumeq2si  36526  prodeq2si  36528  bj-csbsn  37353  csbrecsg  37786  csbrdgg  37787  csboprabg  37788  csbmpo123  37789  csbfinxpg  37846  poimirlem24  38107  cdleme31so  40967  cdleme31sn  40968  cdleme31sn1  40969  cdleme31se  40970  cdleme31se2  40971  cdleme31sc  40972  cdleme31sde  40973  cdleme31sn2  40977  cdlemkid3N  41521  cdlemkid4  41522  climinf2mpt  46252  climinfmpt  46253