Theorem csbeq1d 3132

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

Syntax hints:   → wi 4   = wceq 1395  ⦋csb 3125

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-sbc 3030  df-csb 3126

This theorem is referenced by:  csbidmg  3182  csbco3g  3184  fmptcof  5810  mpomptsx  6357  dmmpossx  6359  fmpox  6360  fmpoco  6376  xpf1o  7025  summodclem3  11934  summodclem2a  11935  summodc  11937  zsumdc  11938  fsum3  11941  sumsnf  11963  fsumcnv  11991  fisumcom2  11992  fsumshftm  11999  fisum0diag2  12001  prodmodclem3  12129  prodmodclem2a  12130  prodmodc  12132  zproddc  12133  fprodseq  12137  prodsnf  12146  fprodcnv  12179  fprodcom2fi  12180  pcmpt  12909  ctiunctlemu1st  13048  ctiunctlemu2nd  13049  ctiunctlemudc  13051  ctiunctlemfo  13053  prdsex  13345  imasex  13381  psrval  14673  fsumdvdsmul  15708