Theorem csbeq2i 2946

Description: Formula-building inference rule 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 2945	. 2 ⊢ (⊤ → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)
4	3	trud 1296	1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶

Syntax hints:   = wceq 1287  ⊤wtru 1288  ⦋csb 2922

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-11 1440  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-sbc 2830  df-csb 2923

This theorem is referenced by:  csbvarg  2947  csbnest1g  2972  csbsng  3486  csbunig  3644  csbxpg  4487  csbcnvg  4588  csbdmg  4598  csbresg  4684  csbrng  4858  csbfv12g  5303  csbnegg  7624  iseqf1olemjpcl  9828  iseqf1olemqpcl  9829  iseqf1olemfvp  9830  iseqf1olemqsum  9833