Theorem eceq1d 6566

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

Syntax hints:   → wi 4   = wceq 1353  [cec 6528

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  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-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133  df-in 3135  df-ss 3142  df-sn 3598  df-pr 3599  df-op 3601  df-br 4002  df-opab 4063  df-xp 4630  df-cnv 4632  df-dm 4634  df-rn 4635  df-res 4636  df-ima 4637  df-ec 6532

This theorem is referenced by:  brecop  6620  eroveu  6621  th3qlem1  6632  th3qlem2  6633  th3q  6635  oviec  6636  ecovcom  6637  ecovicom  6638  ecovass  6639  ecoviass  6640  ecovdi  6641  ecovidi  6642  mulidnq  7383  recexnq  7384  ltexnqq  7402  archnqq  7411  prarloclemarch2  7413  addnq0mo  7441  mulnq0mo  7442  addnnnq0  7443  mulnnnq0  7444  nqnq0a  7448  nqnq0m  7449  nq0a0  7451  nnanq0  7452  distrnq0  7453  mulcomnq0  7454  addassnq0  7456  addpinq1  7458  nq02m  7459  prarloclemlo  7488  prarloclem3  7491  prarloclem5  7494  caucvgprlemnkj  7660  caucvgprlemnbj  7661  caucvgprlemm  7662  caucvgprlemdisj  7668  caucvgprlemloc  7669  caucvgprlemcl  7670  caucvgprlemladdfu  7671  caucvgprlemladdrl  7672  caucvgprlem1  7673  caucvgprlem2  7674  caucvgpr  7676  caucvgprprlemell  7679  caucvgprprlemelu  7680  caucvgprprlemcbv  7681  caucvgprprlemval  7682  caucvgprprlemnkeqj  7684  caucvgprprlemmu  7689  caucvgprprlemopl  7691  caucvgprprlemlol  7692  caucvgprprlemopu  7693  caucvgprprlemloc  7697  caucvgprprlemclphr  7699  caucvgprprlemexbt  7700  caucvgprprlem1  7703  caucvgprprlem2  7704  addsrmo  7737  mulsrmo  7738  addsrpr  7739  mulsrpr  7740  prsrriota  7782  caucvgsrlemfv  7785  caucvgsr  7796  suplocsrlemb  7800  suplocsrlempr  7801  suplocsrlem  7802  suplocsr  7803  pitonnlem2  7841  pitonn  7842  nntopi  7888  axcaucvglemval  7891