Theorem csbeq2i 4026

Description: Formula-building inference rule 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 4025	. 2 ⊢ (⊤ → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)
4	3	trud 1533	1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶

Syntax hints:   = wceq 1523  ⊤wtru 1524  ⦋csb 3566

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-sbc 3469  df-csb 3567

This theorem is referenced by:  csbnest1g  4034  csbvarg  4036  csbsng  4275  csbprg  4276  csbopg  4451  csbuni  4498  csbmpt12  5039  csbxp  5234  csbcnv  5338  csbcnvgALT  5339  csbdm  5350  csbres  5431  csbrn  5631  csbfv12  6269  fvmpt2curryd  7442  csbnegg  10316  csbwrdg  13366  matgsum  20291  disjxpin  29527  f1od2  29627  bj-csbsn  33024  csbpredg  33302  csbwrecsg  33303  csbrecsg  33304  csbrdgg  33305  csboprabg  33306  csbmpt22g  33307  csbfinxpg  33355  poimirlem24  33563  cdleme31so  35984  cdleme31sn  35985  cdleme31sn1  35986  cdleme31se  35987  cdleme31se2  35988  cdleme31sc  35989  cdleme31sde  35990  cdleme31sn2  35994  cdlemkid3N  36538  cdlemkid4  36539  csbxpgOLD  39368  csbresgOLD  39370  csbrngOLD  39371  climinf2mpt  40264  climinfmpt  40265