Theorem csbeq1d 3066

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 3062	. 2 ⊢ (𝐴 = 𝐵 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶)
3	1, 2	syl 14	1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶)

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

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-sbc 2965  df-csb 3060

This theorem is referenced by:  csbidmg  3115  csbco3g  3117  fmptcof  5685  mpomptsx  6200  dmmpossx  6202  fmpox  6203  fmpoco  6219  xpf1o  6846  summodclem3  11390  summodclem2a  11391  summodc  11393  zsumdc  11394  fsum3  11397  sumsnf  11419  fsumcnv  11447  fisumcom2  11448  fsumshftm  11455  fisum0diag2  11457  prodmodclem3  11585  prodmodclem2a  11586  prodmodc  11588  zproddc  11589  fprodseq  11593  prodsnf  11602  fprodcnv  11635  fprodcom2fi  11636  pcmpt  12343  ctiunctlemu1st  12437  ctiunctlemu2nd  12438  ctiunctlemudc  12440  ctiunctlemfo  12442  prdsex  12723  imasex  12731