Theorem csbeq2i 3887

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-sbc 3771  df-csb 3880

This theorem is referenced by:  csbnest1g  4412  csbvarg  4414  csbsng  4689  csbprg  4690  csbopg  4872  csbuni  4917  csbmpt12  5537  csbxp  5759  csbcnv  5868  csbcnvgALT  5869  csbdm  5882  csbres  5974  csbrn  6197  csbpredg  6301  csbfv12  6929  fvmpocurryd  8275  csbfrecsg  8288  csbwrecsg  8325  csbnegg  11484  csbwrdg  14567  matgsum  22380  precsexlemcbv  28165  precsexlem3  28168  disjxpin  32574  f1od2  32703  sumeq2si  36225  prodeq2si  36227  bj-csbsn  36927  csbrecsg  37351  csbrdgg  37352  csboprabg  37353  csbmpo123  37354  csbfinxpg  37411  poimirlem24  37673  cdleme31so  40403  cdleme31sn  40404  cdleme31sn1  40405  cdleme31se  40406  cdleme31se2  40407  cdleme31sc  40408  cdleme31sde  40409  cdleme31sn2  40413  cdlemkid3N  40957  cdlemkid4  40958  climinf2mpt  45710  climinfmpt  45711