Theorem csbeq2i 3916

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-sbc 3792  df-csb 3909

This theorem is referenced by:  csbnest1g  4438  csbvarg  4440  csbsng  4713  csbprg  4714  csbopg  4896  csbuni  4941  csbmpt12  5567  csbxp  5788  csbcnv  5897  csbcnvgALT  5898  csbdm  5911  csbres  6003  csbrn  6225  csbpredg  6329  csbfv12  6955  fvmpocurryd  8295  csbfrecsg  8308  csbwrecsg  8345  csbnegg  11503  csbwrdg  14579  matgsum  22459  precsexlemcbv  28245  precsexlem3  28248  disjxpin  32608  f1od2  32739  sumeq2si  36184  prodeq2si  36186  bj-csbsn  36887  csbrecsg  37311  csbrdgg  37312  csboprabg  37313  csbmpo123  37314  csbfinxpg  37371  poimirlem24  37631  cdleme31so  40362  cdleme31sn  40363  cdleme31sn1  40364  cdleme31se  40365  cdleme31se2  40366  cdleme31sc  40367  cdleme31sde  40368  cdleme31sn2  40372  cdlemkid3N  40916  cdlemkid4  40917  climinf2mpt  45670  climinfmpt  45671