Theorem eceq1d 6663

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 6662	. 2 ⊢ (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶)
3	1, 2	syl 14	1 ⊢ (𝜑 → [𝐴]𝐶 = [𝐵]𝐶)

Syntax hints:   → wi 4   = wceq 1373  [cec 6625

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-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-un 3171  df-in 3173  df-ss 3180  df-sn 3640  df-pr 3641  df-op 3643  df-br 4048  df-opab 4110  df-xp 4685  df-cnv 4687  df-dm 4689  df-rn 4690  df-res 4691  df-ima 4692  df-ec 6629

This theorem is referenced by:  brecop  6719  eroveu  6720  th3qlem1  6731  th3qlem2  6732  th3q  6734  oviec  6735  ecovcom  6736  ecovicom  6737  ecovass  6738  ecoviass  6739  ecovdi  6740  ecovidi  6741  mulidnq  7509  recexnq  7510  ltexnqq  7528  archnqq  7537  prarloclemarch2  7539  addnq0mo  7567  mulnq0mo  7568  addnnnq0  7569  mulnnnq0  7570  nqnq0a  7574  nqnq0m  7575  nq0a0  7577  nnanq0  7578  distrnq0  7579  mulcomnq0  7580  addassnq0  7582  addpinq1  7584  nq02m  7585  prarloclemlo  7614  prarloclem3  7617  prarloclem5  7620  caucvgprlemnkj  7786  caucvgprlemnbj  7787  caucvgprlemm  7788  caucvgprlemdisj  7794  caucvgprlemloc  7795  caucvgprlemcl  7796  caucvgprlemladdfu  7797  caucvgprlemladdrl  7798  caucvgprlem1  7799  caucvgprlem2  7800  caucvgpr  7802  caucvgprprlemell  7805  caucvgprprlemelu  7806  caucvgprprlemcbv  7807  caucvgprprlemval  7808  caucvgprprlemnkeqj  7810  caucvgprprlemmu  7815  caucvgprprlemopl  7817  caucvgprprlemlol  7818  caucvgprprlemopu  7819  caucvgprprlemloc  7823  caucvgprprlemclphr  7825  caucvgprprlemexbt  7826  caucvgprprlem1  7829  caucvgprprlem2  7830  addsrmo  7863  mulsrmo  7864  addsrpr  7865  mulsrpr  7866  prsrriota  7908  caucvgsrlemfv  7911  caucvgsr  7922  suplocsrlemb  7926  suplocsrlempr  7927  suplocsrlem  7928  suplocsr  7929  pitonnlem2  7967  pitonn  7968  nntopi  8014  axcaucvglemval  8017  qus0  13615  qusinv  13616  qussub  13617  quscrng  14339