Theorem csbeq2i 3898

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

Syntax hints:   = wceq 1533  ⊤wtru 1534  ⦋csb 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-12 2166  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-sbc 3775  df-csb 3891

This theorem is referenced by:  csbnest1g  4430  csbvarg  4432  csbsng  4713  csbprg  4714  csbopg  4892  csbuni  4939  csbmpt12  5558  csbxp  5776  csbcnv  5885  csbcnvgALT  5886  csbdm  5899  csbres  5987  csbrn  6207  csbpredg  6311  csbfv12  6942  fvmpocurryd  8275  csbfrecsg  8288  csbwrecsg  8325  csbnegg  11487  csbwrdg  14526  matgsum  22369  precsexlemcbv  28138  precsexlem3  28141  disjxpin  32435  f1od2  32560  bj-csbsn  36452  csbrecsg  36877  csbrdgg  36878  csboprabg  36879  csbmpo123  36880  csbfinxpg  36937  poimirlem24  37187  cdleme31so  39921  cdleme31sn  39922  cdleme31sn1  39923  cdleme31se  39924  cdleme31se2  39925  cdleme31sc  39926  cdleme31sde  39927  cdleme31sn2  39931  cdlemkid3N  40475  cdlemkid4  40476  climinf2mpt  45165  climinfmpt  45166