Theorem csbeq2i 3121

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

Syntax hints:   = wceq 1373  ⊤wtru 1374  ⦋csb 3094

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-sbc 3000  df-csb 3095

This theorem is referenced by:  csbvarg  3122  csbnest1g  3150  csbsng  3695  csbunig  3860  csbxpg  4760  csbcnvg  4866  csbdmg  4877  csbresg  4967  csbrng  5149  csbfv12g  5621  csbnegg  8277  iseqf1olemjpcl  10660  iseqf1olemqpcl  10661  iseqf1olemfvp  10662  seq3f1olemqsum  10665  csbwrdg  11030