Theorem csbeq2i 4219

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

Syntax hints:   = wceq 1656  ⊤wtru 1657  ⦋csb 3757

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-sbc 3663  df-csb 3758

This theorem is referenced by:  csbnest1g  4227  csbvarg  4229  csbsng  4464  csbprg  4465  csbopg  4643  csbuni  4690  csbmpt12  5238  csbxp  5439  csbcnv  5542  csbcnvgALT  5543  csbdm  5554  csbres  5636  csbrn  5841  csbfv12  6481  fvmpt2curryd  7667  csbnegg  10605  csbwrdg  13611  matgsum  20617  disjxpin  29944  f1od2  30043  bj-csbsn  33419  csbpredg  33717  csbwrecsg  33718  csbrecsg  33719  csbrdgg  33720  csboprabg  33721  csbmpt22g  33722  csbfinxpg  33769  poimirlem24  33976  cdleme31so  36453  cdleme31sn  36454  cdleme31sn1  36455  cdleme31se  36456  cdleme31se2  36457  cdleme31sc  36458  cdleme31sde  36459  cdleme31sn2  36463  cdlemkid3N  37007  cdlemkid4  37008  climinf2mpt  40739  climinfmpt  40740