Theorem eceq1d 6165

Description: Equality theorem for equivalence class (deduction form). (Contributed by Jim Kingdon, 31-Dec-2019.)

Hypothesis

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

Assertion

Ref	Expression
eceq1d	⊢ (𝜑 → [𝐴]𝐶 = [𝐵]𝐶)

Proof of Theorem eceq1d

Step	Hyp	Ref	Expression
1		eceq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eceq1 6164	. 2 ⊢ (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶)
3	1, 2	syl 14	1 ⊢ (𝜑 → [𝐴]𝐶 = [𝐵]𝐶)

Syntax hints:   → wi 4   = wceq 1284  [cec 6127

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-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-3an 921  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-v 2603  df-un 2977  df-in 2979  df-ss 2986  df-sn 3404  df-pr 3405  df-op 3407  df-br 3786  df-opab 3840  df-xp 4369  df-cnv 4371  df-dm 4373  df-rn 4374  df-res 4375  df-ima 4376  df-ec 6131

This theorem is referenced by:  brecop  6219  eroveu  6220  th3qlem1  6231  th3qlem2  6232  th3q  6234  oviec  6235  ecovcom  6236  ecovicom  6237  ecovass  6238  ecoviass  6239  ecovdi  6240  ecovidi  6241  mulidnq  6579  recexnq  6580  ltexnqq  6598  archnqq  6607  prarloclemarch2  6609  addnq0mo  6637  mulnq0mo  6638  addnnnq0  6639  mulnnnq0  6640  nqnq0a  6644  nqnq0m  6645  nq0a0  6647  nnanq0  6648  distrnq0  6649  mulcomnq0  6650  addassnq0  6652  addpinq1  6654  nq02m  6655  prarloclemlo  6684  prarloclem3  6687  prarloclem5  6690  caucvgprlemnkj  6856  caucvgprlemnbj  6857  caucvgprlemm  6858  caucvgprlemdisj  6864  caucvgprlemloc  6865  caucvgprlemcl  6866  caucvgprlemladdfu  6867  caucvgprlemladdrl  6868  caucvgprlem1  6869  caucvgprlem2  6870  caucvgpr  6872  caucvgprprlemell  6875  caucvgprprlemelu  6876  caucvgprprlemcbv  6877  caucvgprprlemval  6878  caucvgprprlemnkeqj  6880  caucvgprprlemmu  6885  caucvgprprlemopl  6887  caucvgprprlemlol  6888  caucvgprprlemopu  6889  caucvgprprlemloc  6893  caucvgprprlemclphr  6895  caucvgprprlemexbt  6896  caucvgprprlem1  6899  caucvgprprlem2  6900  addsrmo  6920  mulsrmo  6921  addsrpr  6922  mulsrpr  6923  prsrriota  6964  caucvgsrlemfv  6967  caucvgsr  6978  pitonnlem2  7015  pitonn  7016  nntopi  7060  axcaucvglemval  7063