Theorem csbeq2i 3863

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

Syntax hints:   = wceq 1563  ⊤wtru 1564  ⦋csb 3855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-sbc 3748  df-csb 3856

This theorem is referenced by:  csbnest1g  4389  csbvarg  4391  csbsng  4670  csbprg  4671  csbopg  4852  csbuni  4899  csbmpt12  5533  csbxp  5753  csbcnv  5863  csbcnvOLD  5864  csbcnvgALTOLD  5865  csbdm  5878  csbres  5972  csbrn  6194  csbpredg  6298  csbfv12  6916  fvmpocurryd  8255  csbfrecsg  8269  csbwrecsg  8303  csbnegg  11442  csbwrdg  14571  matgsum  22555  precsexlemcbv  28357  precsexlem3  28360  disjxpin  32843  f1od2  32976  sumeq2si  36575  prodeq2si  36577  bj-csbsn  37401  csbrecsg  37834  csbrdgg  37835  csboprabg  37836  csbmpo123  37837  csbfinxpg  37894  poimirlem24  38155  cdleme31so  41015  cdleme31sn  41016  cdleme31sn1  41017  cdleme31se  41018  cdleme31se2  41019  cdleme31sc  41020  cdleme31sde  41021  cdleme31sn2  41025  cdlemkid3N  41569  cdlemkid4  41570  climinf2mpt  46286  climinfmpt  46287