Theorem csbeq2i 3862

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

Syntax hints:   = wceq 1570  ⊤wtru 1571  ⦋csb 3854

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-sbc 3746  df-csb 3855

This theorem is referenced by:  csbnest1g  4398  csbvarg  4400  csbsng  4675  csbprg  4676  csbopg  4857  csbuni  4904  csbmpt12  5544  csbxp  5764  csbcnv  5874  csbcnvOLD  5875  csbcnvgALTOLD  5876  csbdm  5889  csbres  5983  csbrn  6206  csbpredg  6310  csbfv12  6928  fvmpocurryd  8268  csbfrecsg  8282  csbwrecsg  8316  csbnegg  11455  csbwrdg  14583  matgsum  22575  precsexlemcbv  28380  precsexlem3  28383  disjxpin  32914  f1od2  33045  sumeq2si  36695  prodeq2si  36697  bj-csbsn  37520  csbrecsg  37955  csbrdgg  37956  csboprabg  37957  csbmpo123  37958  csbfinxpg  38015  poimirlem24  38276  cdleme31so  41134  cdleme31sn  41135  cdleme31sn1  41136  cdleme31se  41137  cdleme31se2  41138  cdleme31sc  41139  cdleme31sde  41140  cdleme31sn2  41144  cdlemkid3N  41688  cdlemkid4  41689  climinf2mpt  46411  climinfmpt  46412