Theorem csbeq2i 3869

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

Syntax hints:   = wceq 1567  ⊤wtru 1568  ⦋csb 3861

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-sbc 3754  df-csb 3862

This theorem is referenced by:  csbnest1g  4403  csbvarg  4405  csbsng  4679  csbprg  4680  csbopg  4860  csbuni  4907  csbmpt12  5543  csbxp  5763  csbcnv  5873  csbcnvOLD  5874  csbcnvgALTOLD  5875  csbdm  5888  csbres  5982  csbrn  6205  csbpredg  6309  csbfv12  6927  fvmpocurryd  8266  csbfrecsg  8280  csbwrecsg  8314  csbnegg  11453  csbwrdg  14580  matgsum  22562  precsexlemcbv  28364  precsexlem3  28367  disjxpin  32873  f1od2  33004  sumeq2si  36602  prodeq2si  36604  bj-csbsn  37427  csbrecsg  37861  csbrdgg  37862  csboprabg  37863  csbmpo123  37864  csbfinxpg  37921  poimirlem24  38182  cdleme31so  41042  cdleme31sn  41043  cdleme31sn1  41044  cdleme31se  41045  cdleme31se2  41046  cdleme31sc  41047  cdleme31sde  41048  cdleme31sn2  41052  cdlemkid3N  41596  cdlemkid4  41597  climinf2mpt  46319  climinfmpt  46320