Theorem csbeq2i 3857

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

Syntax hints:   = wceq 1541  ⊤wtru 1542  ⦋csb 3849

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-sbc 3741  df-csb 3850

This theorem is referenced by:  csbnest1g  4384  csbvarg  4386  csbsng  4665  csbprg  4666  csbopg  4847  csbuni  4893  csbmpt12  5505  csbxp  5725  csbcnv  5832  csbcnvgALT  5833  csbdm  5846  csbres  5941  csbrn  6161  csbpredg  6265  csbfv12  6879  fvmpocurryd  8213  csbfrecsg  8226  csbwrecsg  8260  csbnegg  11377  csbwrdg  14467  matgsum  22381  precsexlemcbv  28202  precsexlem3  28205  disjxpin  32663  f1od2  32798  sumeq2si  36396  prodeq2si  36398  bj-csbsn  37105  csbrecsg  37529  csbrdgg  37530  csboprabg  37531  csbmpo123  37532  csbfinxpg  37589  poimirlem24  37841  cdleme31so  40635  cdleme31sn  40636  cdleme31sn1  40637  cdleme31se  40638  cdleme31se2  40639  cdleme31sc  40640  cdleme31sde  40641  cdleme31sn2  40645  cdlemkid3N  41189  cdlemkid4  41190  climinf2mpt  45954  climinfmpt  45955