Theorem csbeq2i 3864

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

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

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 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-sbc 3748  df-csb 3857

This theorem is used by:  csbnest1g  4400  csbvarg  4402  csbsng  4679  csbprg  4680  csbopg  4861  csbuni  4908  csbmpt12  5547  csbxp  5767  csbcnv  5877  csbcnvOLD  5878  csbcnvgALTOLD  5879  csbdm  5892  csbres  5986  csbrn  6209  csbpredg  6315  csbfv12  6933  fvmpocurryd  8276  csbfrecsg  8290  csbwrecsg  8324  csbnegg  11472  csbwrdg  14601  matgsum  22631  precsexlemcbv  28436  precsexlem3  28439  disjxpin  32970  f1od2  33101  sumeq2si  36755  prodeq2si  36757  bj-csbsn  37580  csbrecsg  38015  csbrdgg  38016  csboprabg  38017  csbmpo123  38018  csbfinxpg  38075  poimirlem24  38336  cdleme31so  41194  cdleme31sn  41195  cdleme31sn1  41196  cdleme31se  41197  cdleme31se2  41198  cdleme31sc  41199  cdleme31sde  41200  cdleme31sn2  41204  cdlemkid3N  41748  cdlemkid4  41749  climinf2mpt  46469  climinfmpt  46470