Theorem csbeq2i 3893

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

Syntax hints:   = wceq 1537  ⊤wtru 1538  ⦋csb 3885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-sbc 3775  df-csb 3886

This theorem is referenced by:  csbnest1g  4383  csbvarg  4385  csbsng  4646  csbprg  4647  csbopg  4823  csbuni  4869  csbmpt12  5446  csbxp  5652  csbcnv  5756  csbcnvgALT  5757  csbdm  5768  csbres  5858  csbrn  6062  csbfv12  6715  fvmpocurryd  7939  csbnegg  10885  csbwrdg  13897  matgsum  21048  disjxpin  30340  f1od2  30459  bj-csbsn  34223  csbpredg  34609  csbwrecsg  34610  csbrecsg  34611  csbrdgg  34612  csboprabg  34613  csbmpo123  34614  csbfinxpg  34671  poimirlem24  34918  cdleme31so  37517  cdleme31sn  37518  cdleme31sn1  37519  cdleme31se  37520  cdleme31se2  37521  cdleme31sc  37522  cdleme31sde  37523  cdleme31sn2  37527  cdlemkid3N  38071  cdlemkid4  38072  climinf2mpt  42002  climinfmpt  42003