Theorem csbeq2i 3858

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

This proof depends on syntax axioms:   = wceq 1570  ⊤wtru 1571  ⦋csb 3850

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-sbc 3743  df-csb 3851

This theorem is used by:  csbnest1g  4393  csbvarg  4395  csbsng  4672  csbprg  4673  csbopg  4854  csbuni  4901  csbmpt12  5540  csbxp  5760  csbcnv  5870  csbcnvOLD  5871  csbcnvgALTOLD  5872  csbdm  5885  csbres  5979  csbrn  6203  csbpredg  6309  csbfv12  6927  fvmpocurryd  8273  csbfrecsg  8287  csbwrecsg  8321  csbnegg  11482  csbwrdg  14613  matgsum  22665  precsexlemcbv  28479  precsexlem3  28482  disjxpin  33069  f1od2  33198  sumeq2si  36830  prodeq2si  36832  bj-csbsn  37655  csbrecsg  38090  csbrdgg  38091  csboprabg  38092  csbmpo123  38093  csbfinxpg  38150  poimirlem24  38401  cdleme31so  41260  cdleme31sn  41261  cdleme31sn1  41262  cdleme31se  41263  cdleme31se2  41264  cdleme31sc  41265  cdleme31sde  41266  cdleme31sn2  41270  cdlemkid3N  41814  cdlemkid4  41815  climinf2mpt  46550  climinfmpt  46551