Theorem csbeq2i 3945

Description: Formula-building inference rule 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 3944	. 2 ⊢ (⊤ → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)
4	3	trud 1484	1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶

Syntax hints:   = wceq 1475  ⊤wtru 1476  ⦋csb 3499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-sbc 3403  df-csb 3500

This theorem is referenced by:  csbnest1g  3953  csbvarg  3955  csbsng  4190  csbprg  4191  csbopg  4358  csbuni  4402  csbmpt12  4934  csbxp  5123  csbcnv  5228  csbcnvgALT  5229  csbdm  5240  csbres  5320  csbrn  5514  csbfv12  6141  fvmpt2curryd  7284  csbnegg  10157  csbwrdg  13189  matgsum  20062  disjxpin  28783  bj-csbsn  32091  csbpredg  32348  csbwrecsg  32349  csbrecsg  32350  csbrdgg  32351  csboprabg  32352  csbmpt22g  32353  csbfinxpg  32401  poimirlem24  32603  cdleme31so  34685  cdleme31sn  34686  cdleme31sn1  34687  cdleme31se  34688  cdleme31se2  34689  cdleme31sc  34690  cdleme31sde  34691  cdleme31sn2  34695  cdlemkid3N  35239  cdlemkid4  35240  csbunigOLD  38073  csbfv12gALTOLD  38074  csbxpgOLD  38075  csbresgOLD  38077  csbrngOLD  38078  csbima12gALTOLD  38079