Theorem csbeq2i 3859

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-sbc 3743  df-csb 3852

This theorem is used by:  csbnest1g  4393  csbvarg  4395  csbsng  4669  csbprg  4670  csbopg  4854  csbuni  4901  csbmpt12  5537  csbxp  5758  csbcnv  5872  csbcnvOLD  5873  csbcnvgALTOLD  5874  csbdm  5887  csbres  5985  csbrn  6218  csbpredg  6331  csbfv12  6956  f1od2  8138  fvmpocurryd  8319  csbfrecsg  8333  csbwrecsg  8367  csbnegg  11584  csbwrdg  14719  matgsum  22785  precsexlemcbv  28625  precsexlem3  28628  disjxpin  33257  sumeq2si  37182  prodeq2si  37184  bj-csbsn  38007  csbrecsg  38456  csbrdgg  38457  csboprabg  38458  csbmpo123  38459  csbfinxpg  38516  poimirlem24  38767  cdleme31so  41639  cdleme31sn  41640  cdleme31sn1  41641  cdleme31se  41642  cdleme31se2  41643  cdleme31sc  41644  cdleme31sde  41645  cdleme31sn2  41649  cdlemkid3N  42193  cdlemkid4  42194  climinf2mpt  46939  climinfmpt  46940