Theorem csbeq1d 3062

Description: Equality deduction for proper substitution into a class. (Contributed by NM, 3-Dec-2005.)

Hypothesis

Ref	Expression
csbeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
csbeq1d	⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶)

Proof of Theorem csbeq1d

Step	Hyp	Ref	Expression
1		csbeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		csbeq1 3058	. 2 ⊢ (𝐴 = 𝐵 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶)
3	1, 2	syl 14	1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶)

Syntax hints:   → wi 4   = wceq 1353  ⦋csb 3055

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 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-11 1504  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-sbc 2961  df-csb 3056

This theorem is referenced by:  csbidmg  3111  csbco3g  3113  fmptcof  5675  mpomptsx  6188  dmmpossx  6190  fmpox  6191  fmpoco  6207  xpf1o  6834  summodclem3  11354  summodclem2a  11355  summodc  11357  zsumdc  11358  fsum3  11361  sumsnf  11383  fsumcnv  11411  fisumcom2  11412  fsumshftm  11419  fisum0diag2  11421  prodmodclem3  11549  prodmodclem2a  11550  prodmodc  11552  zproddc  11553  fprodseq  11557  prodsnf  11566  fprodcnv  11599  fprodcom2fi  11600  pcmpt  12306  ctiunctlemu1st  12400  ctiunctlemu2nd  12401  ctiunctlemudc  12403  ctiunctlemfo  12405