Theorem csbeq2i 3872

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

Syntax hints:   = wceq 1540  ⊤wtru 1541  ⦋csb 3864

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-sbc 3756  df-csb 3865

This theorem is referenced by:  csbnest1g  4397  csbvarg  4399  csbsng  4674  csbprg  4675  csbopg  4857  csbuni  4902  csbmpt12  5519  csbxp  5740  csbcnv  5849  csbcnvgALT  5850  csbdm  5863  csbres  5955  csbrn  6178  csbpredg  6282  csbfv12  6908  fvmpocurryd  8252  csbfrecsg  8265  csbwrecsg  8299  csbnegg  11424  csbwrdg  14515  matgsum  22330  precsexlemcbv  28114  precsexlem3  28117  disjxpin  32523  f1od2  32650  sumeq2si  36185  prodeq2si  36187  bj-csbsn  36887  csbrecsg  37311  csbrdgg  37312  csboprabg  37313  csbmpo123  37314  csbfinxpg  37371  poimirlem24  37633  cdleme31so  40368  cdleme31sn  40369  cdleme31sn1  40370  cdleme31se  40371  cdleme31se2  40372  cdleme31sc  40373  cdleme31sde  40374  cdleme31sn2  40378  cdlemkid3N  40922  cdlemkid4  40923  climinf2mpt  45705  climinfmpt  45706