Theorem csbeq2i 3897

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

Syntax hints:   = wceq 1534  ⊤wtru 1535  ⦋csb 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-12 2164  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-sbc 3775  df-csb 3890

This theorem is referenced by:  csbnest1g  4425  csbvarg  4427  csbsng  4708  csbprg  4709  csbopg  4887  csbuni  4934  csbmpt12  5553  csbxp  5771  csbcnv  5880  csbcnvgALT  5881  csbdm  5894  csbres  5982  csbrn  6201  csbpredg  6305  csbfv12  6939  fvmpocurryd  8270  csbfrecsg  8283  csbwrecsg  8320  csbnegg  11479  csbwrdg  14518  matgsum  22326  precsexlemcbv  28091  precsexlem3  28094  disjxpin  32363  f1od2  32487  bj-csbsn  36318  csbrecsg  36743  csbrdgg  36744  csboprabg  36745  csbmpo123  36746  csbfinxpg  36803  poimirlem24  37052  cdleme31so  39789  cdleme31sn  39790  cdleme31sn1  39791  cdleme31se  39792  cdleme31se2  39793  cdleme31sc  39794  cdleme31sde  39795  cdleme31sn2  39799  cdlemkid3N  40343  cdlemkid4  40344  climinf2mpt  45025  climinfmpt  45026