Theorem csbeq1d 3133

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

Syntax hints:   → wi 4   = wceq 1397  ⦋csb 3126

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-sbc 3031  df-csb 3127

This theorem is referenced by:  csbidmg  3183  csbco3g  3185  fmptcof  5817  mpomptsx  6367  dmmpossx  6369  fmpox  6370  fmpoco  6386  xpf1o  7035  summodclem3  11964  summodclem2a  11965  summodc  11967  zsumdc  11968  fsum3  11971  sumsnf  11993  fsumcnv  12021  fisumcom2  12022  fsumshftm  12029  fisum0diag2  12031  prodmodclem3  12159  prodmodclem2a  12160  prodmodc  12162  zproddc  12163  fprodseq  12167  prodsnf  12176  fprodcnv  12209  fprodcom2fi  12210  pcmpt  12939  ctiunctlemu1st  13078  ctiunctlemu2nd  13079  ctiunctlemudc  13081  ctiunctlemfo  13083  prdsex  13375  imasex  13411  psrval  14704  fsumdvdsmul  15744