Theorem csbeq2i 3854

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

This proof depends on syntax axioms:   = wceq 1569  ⊤wtru 1570  ⦋csb 3846

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-sbc 3739  df-csb 3847

This theorem is used by:  csbnest1g  4389  csbvarg  4391  csbsng  4665  csbprg  4666  csbopg  4850  csbuni  4897  csbmpt12  5531  csbxp  5751  csbcnv  5863  csbcnvOLD  5864  csbcnvgALTOLD  5865  csbdm  5878  csbres  5972  csbrn  6204  csbpredg  6310  csbfv12  6931  f1od2  8111  fvmpocurryd  8292  csbfrecsg  8306  csbwrecsg  8340  csbnegg  11558  csbwrdg  14693  matgsum  22758  precsexlemcbv  28598  precsexlem3  28601  disjxpin  33230  sumeq2si  37084  prodeq2si  37086  bj-csbsn  37909  csbrecsg  38345  csbrdgg  38346  csboprabg  38347  csbmpo123  38348  csbfinxpg  38405  poimirlem24  38656  cdleme31so  41530  cdleme31sn  41531  cdleme31sn1  41532  cdleme31se  41533  cdleme31se2  41534  cdleme31sc  41535  cdleme31sde  41536  cdleme31sn2  41540  cdlemkid3N  42084  cdlemkid4  42085  climinf2mpt  46818  climinfmpt  46819