Theorem csbeq2i 3902

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

Syntax hints:   = wceq 1542  ⊤wtru 1543  ⦋csb 3894

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-sbc 3779  df-csb 3895

This theorem is referenced by:  csbnest1g  4430  csbvarg  4432  csbsng  4713  csbprg  4714  csbopg  4892  csbuni  4941  csbmpt12  5558  csbxp  5776  csbcnv  5884  csbcnvgALT  5885  csbdm  5898  csbres  5985  csbrn  6203  csbpredg  6307  csbfv12  6940  fvmpocurryd  8256  csbfrecsg  8269  csbwrecsg  8306  csbnegg  11457  csbwrdg  14494  matgsum  21939  precsexlemcbv  27652  precsexlem3  27655  disjxpin  31819  f1od2  31946  bj-csbsn  35784  csbrecsg  36209  csbrdgg  36210  csboprabg  36211  csbmpo123  36212  csbfinxpg  36269  poimirlem24  36512  cdleme31so  39250  cdleme31sn  39251  cdleme31sn1  39252  cdleme31se  39253  cdleme31se2  39254  cdleme31sc  39255  cdleme31sde  39256  cdleme31sn2  39260  cdlemkid3N  39804  cdlemkid4  39805  climinf2mpt  44430  climinfmpt  44431