Theorem csbeq2i 3901

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-12 2171  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-sbc 3778  df-csb 3894

This theorem is referenced by:  csbnest1g  4429  csbvarg  4431  csbsng  4712  csbprg  4713  csbopg  4891  csbuni  4940  csbmpt12  5557  csbxp  5775  csbcnv  5883  csbcnvgALT  5884  csbdm  5897  csbres  5984  csbrn  6202  csbpredg  6306  csbfv12  6939  fvmpocurryd  8258  csbfrecsg  8271  csbwrecsg  8308  csbnegg  11461  csbwrdg  14498  matgsum  22159  precsexlemcbv  27879  precsexlem3  27882  disjxpin  32074  f1od2  32201  bj-csbsn  36087  csbrecsg  36512  csbrdgg  36513  csboprabg  36514  csbmpo123  36515  csbfinxpg  36572  poimirlem24  36815  cdleme31so  39553  cdleme31sn  39554  cdleme31sn1  39555  cdleme31se  39556  cdleme31se2  39557  cdleme31sc  39558  cdleme31sde  39559  cdleme31sn2  39563  cdlemkid3N  40107  cdlemkid4  40108  climinf2mpt  44729  climinfmpt  44730