Theorem csbeq2i 3855

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

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

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-sbc 3740  df-csb 3848

This theorem is used by:  csbnest1g  4390  csbvarg  4392  csbsng  4669  csbprg  4670  csbopg  4851  csbuni  4898  csbmpt12  5532  csbxp  5752  csbcnv  5864  csbcnvOLD  5865  csbcnvgALTOLD  5866  csbdm  5879  csbres  5973  csbrn  6197  csbpredg  6303  csbfv12  6922  fvmpocurryd  8272  csbfrecsg  8286  csbwrecsg  8320  csbnegg  11535  csbwrdg  14669  matgsum  22732  precsexlemcbv  28574  precsexlem3  28577  disjxpin  33164  f1od2  33293  sumeq2si  36961  prodeq2si  36963  bj-csbsn  37786  csbrecsg  38219  csbrdgg  38220  csboprabg  38221  csbmpo123  38222  csbfinxpg  38279  poimirlem24  38530  cdleme31so  41404  cdleme31sn  41405  cdleme31sn1  41406  cdleme31se  41407  cdleme31se2  41408  cdleme31sc  41409  cdleme31sde  41410  cdleme31sn2  41414  cdlemkid3N  41958  cdlemkid4  41959  climinf2mpt  46668  climinfmpt  46669