Theorem csbeq2i 3836

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

Syntax hints:   = wceq 1539  ⊤wtru 1540  ⦋csb 3828

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-sbc 3712  df-csb 3829

This theorem is referenced by:  csbnest1g  4360  csbvarg  4362  csbsng  4641  csbprg  4642  csbopg  4819  csbuni  4867  csbmpt12  5463  csbxp  5676  csbcnv  5781  csbcnvgALT  5782  csbdm  5795  csbres  5883  csbrn  6095  csbpredg  6197  csbfv12  6799  fvmpocurryd  8058  csbfrecsg  8071  csbwrecsg  8108  csbnegg  11148  csbwrdg  14175  matgsum  21494  disjxpin  30828  f1od2  30958  bj-csbsn  35016  csbrecsg  35426  csbrdgg  35427  csboprabg  35428  csbmpo123  35429  csbfinxpg  35486  poimirlem24  35728  cdleme31so  38320  cdleme31sn  38321  cdleme31sn1  38322  cdleme31se  38323  cdleme31se2  38324  cdleme31sc  38325  cdleme31sde  38326  cdleme31sn2  38330  cdlemkid3N  38874  cdlemkid4  38875  climinf2mpt  43145  climinfmpt  43146