Theorem csbeq2i 3870

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-sbc 3754  df-csb 3863

This theorem is referenced by:  csbnest1g  4395  csbvarg  4397  csbsng  4672  csbprg  4673  csbopg  4855  csbuni  4900  csbmpt12  5517  csbxp  5738  csbcnv  5847  csbcnvgALT  5848  csbdm  5861  csbres  5953  csbrn  6176  csbpredg  6280  csbfv12  6906  fvmpocurryd  8250  csbfrecsg  8263  csbwrecsg  8297  csbnegg  11418  csbwrdg  14509  matgsum  22324  precsexlemcbv  28108  precsexlem3  28111  disjxpin  32517  f1od2  32644  sumeq2si  36190  prodeq2si  36192  bj-csbsn  36892  csbrecsg  37316  csbrdgg  37317  csboprabg  37318  csbmpo123  37319  csbfinxpg  37376  poimirlem24  37638  cdleme31so  40373  cdleme31sn  40374  cdleme31sn1  40375  cdleme31se  40376  cdleme31se2  40377  cdleme31sc  40378  cdleme31sde  40379  cdleme31sn2  40383  cdlemkid3N  40927  cdlemkid4  40928  climinf2mpt  45712  climinfmpt  45713