Theorem csbeq2i 3887

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

Syntax hints:   = wceq 1539  ⊤wtru 1540  ⦋csb 3879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-sbc 3771  df-csb 3880

This theorem is referenced by:  csbnest1g  4412  csbvarg  4414  csbsng  4688  csbprg  4689  csbopg  4871  csbuni  4916  csbmpt12  5542  csbxp  5765  csbcnv  5874  csbcnvgALT  5875  csbdm  5888  csbres  5980  csbrn  6203  csbpredg  6307  csbfv12  6934  fvmpocurryd  8278  csbfrecsg  8291  csbwrecsg  8328  csbnegg  11487  csbwrdg  14564  matgsum  22391  precsexlemcbv  28166  precsexlem3  28169  disjxpin  32536  f1od2  32667  sumeq2si  36162  prodeq2si  36164  bj-csbsn  36864  csbrecsg  37288  csbrdgg  37289  csboprabg  37290  csbmpo123  37291  csbfinxpg  37348  poimirlem24  37610  cdleme31so  40340  cdleme31sn  40341  cdleme31sn1  40342  cdleme31se  40343  cdleme31se2  40344  cdleme31sc  40345  cdleme31sde  40346  cdleme31sn2  40350  cdlemkid3N  40894  cdlemkid4  40895  climinf2mpt  45686  climinfmpt  45687