Theorem csbeq2i 3890

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

Syntax hints:   = wceq 1533  ⊤wtru 1534  ⦋csb 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-sbc 3772  df-csb 3883

This theorem is referenced by:  csbnest1g  4380  csbvarg  4382  csbsng  4637  csbprg  4638  csbopg  4814  csbuni  4859  csbmpt12  5436  csbxp  5644  csbcnv  5748  csbcnvgALT  5749  csbdm  5760  csbres  5850  csbrn  6054  csbfv12  6707  fvmpocurryd  7931  csbnegg  10877  csbwrdg  13889  matgsum  21040  disjxpin  30332  f1od2  30451  bj-csbsn  34216  csbpredg  34601  csbwrecsg  34602  csbrecsg  34603  csbrdgg  34604  csboprabg  34605  csbmpo123  34606  csbfinxpg  34663  poimirlem24  34910  cdleme31so  37509  cdleme31sn  37510  cdleme31sn1  37511  cdleme31se  37512  cdleme31se2  37513  cdleme31sc  37514  cdleme31sde  37515  cdleme31sn2  37519  cdlemkid3N  38063  cdlemkid4  38064  climinf2mpt  41988  climinfmpt  41989