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  4851  csbuni  4898  csbmpt12  5532  csbxp  5752  csbcnv  5862  csbcnvOLD  5863  csbcnvgALTOLD  5864  csbdm  5877  csbres  5971  csbrn  6193  csbpredg  6297  csbfv12  6916  fvmpocurryd  8255  csbfrecsg  8269  csbwrecsg  8303  csbnegg  11442  csbwrdg  14569  matgsum  22551  precsexlemcbv  28353  precsexlem3  28356  disjxpin  32839  f1od2  32972  sumeq2si  36570  prodeq2si  36572  bj-csbsn  37396  csbrecsg  37829  csbrdgg  37830  csboprabg  37831  csbmpo123  37832  csbfinxpg  37889  poimirlem24  38150  cdleme31so  41010  cdleme31sn  41011  cdleme31sn1  41012  cdleme31se  41013  cdleme31se2  41014  cdleme31sc  41015  cdleme31sde  41016  cdleme31sn2  41020  cdlemkid3N  41564  cdlemkid4  41565  climinf2mpt  46287  climinfmpt  46288