Theorem csbeq2i 3836

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

Syntax hints:   = wceq 1538  ⊤wtru 1539  ⦋csb 3828

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-sbc 3721  df-csb 3829

This theorem is referenced by:  csbnest1g  4337  csbvarg  4339  csbsng  4604  csbprg  4605  csbopg  4783  csbuni  4829  csbmpt12  5409  csbxp  5614  csbcnv  5718  csbcnvgALT  5719  csbdm  5730  csbres  5821  csbrn  6027  csbfv12  6688  fvmpocurryd  7920  csbnegg  10872  csbwrdg  13887  matgsum  21042  disjxpin  30351  f1od2  30483  bj-csbsn  34345  csbpredg  34743  csbwrecsg  34744  csbrecsg  34745  csbrdgg  34746  csboprabg  34747  csbmpo123  34748  csbfinxpg  34805  poimirlem24  35081  cdleme31so  37675  cdleme31sn  37676  cdleme31sn1  37677  cdleme31se  37678  cdleme31se2  37679  cdleme31sc  37680  cdleme31sde  37681  cdleme31sn2  37685  cdlemkid3N  38229  cdlemkid4  38230  climinf2mpt  42356  climinfmpt  42357