Theorem csbeq2i 3907

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

Syntax hints:   = wceq 1540  ⊤wtru 1541  ⦋csb 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-sbc 3789  df-csb 3900

This theorem is referenced by:  csbnest1g  4432  csbvarg  4434  csbsng  4708  csbprg  4709  csbopg  4891  csbuni  4936  csbmpt12  5562  csbxp  5785  csbcnv  5894  csbcnvgALT  5895  csbdm  5908  csbres  6000  csbrn  6223  csbpredg  6327  csbfv12  6954  fvmpocurryd  8296  csbfrecsg  8309  csbwrecsg  8346  csbnegg  11505  csbwrdg  14582  matgsum  22443  precsexlemcbv  28230  precsexlem3  28233  disjxpin  32601  f1od2  32732  sumeq2si  36203  prodeq2si  36205  bj-csbsn  36905  csbrecsg  37329  csbrdgg  37330  csboprabg  37331  csbmpo123  37332  csbfinxpg  37389  poimirlem24  37651  cdleme31so  40381  cdleme31sn  40382  cdleme31sn1  40383  cdleme31se  40384  cdleme31se2  40385  cdleme31sc  40386  cdleme31sde  40387  cdleme31sn2  40391  cdlemkid3N  40935  cdlemkid4  40936  climinf2mpt  45729  climinfmpt  45730