Theorem eceq1d 6802

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

Syntax hints:   → wi 4   = wceq 1398  [cec 6764

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2814  df-un 3214  df-in 3216  df-ss 3223  df-sn 3694  df-pr 3695  df-op 3697  df-br 4109  df-opab 4171  df-xp 4754  df-cnv 4756  df-dm 4758  df-rn 4759  df-res 4760  df-ima 4761  df-ec 6768

This theorem is referenced by:  brecop  6858  eroveu  6859  th3qlem1  6870  th3qlem2  6871  th3q  6873  oviec  6874  ecovcom  6875  ecovicom  6876  ecovass  6877  ecoviass  6878  ecovdi  6879  ecovidi  6880  mulidnq  7700  recexnq  7701  ltexnqq  7719  archnqq  7728  prarloclemarch2  7730  addnq0mo  7758  mulnq0mo  7759  addnnnq0  7760  mulnnnq0  7761  nqnq0a  7765  nqnq0m  7766  nq0a0  7768  nnanq0  7769  distrnq0  7770  mulcomnq0  7771  addassnq0  7773  addpinq1  7775  nq02m  7776  prarloclemlo  7805  prarloclem3  7808  prarloclem5  7811  caucvgprlemnkj  7977  caucvgprlemnbj  7978  caucvgprlemm  7979  caucvgprlemdisj  7985  caucvgprlemloc  7986  caucvgprlemcl  7987  caucvgprlemladdfu  7988  caucvgprlemladdrl  7989  caucvgprlem1  7990  caucvgprlem2  7991  caucvgpr  7993  caucvgprprlemell  7996  caucvgprprlemelu  7997  caucvgprprlemcbv  7998  caucvgprprlemval  7999  caucvgprprlemnkeqj  8001  caucvgprprlemmu  8006  caucvgprprlemopl  8008  caucvgprprlemlol  8009  caucvgprprlemopu  8010  caucvgprprlemloc  8014  caucvgprprlemclphr  8016  caucvgprprlemexbt  8017  caucvgprprlem1  8020  caucvgprprlem2  8021  addsrmo  8054  mulsrmo  8055  addsrpr  8056  mulsrpr  8057  prsrriota  8099  caucvgsrlemfv  8102  caucvgsr  8113  suplocsrlemb  8117  suplocsrlempr  8118  suplocsrlem  8119  suplocsr  8120  pitonnlem2  8158  pitonn  8159  nntopi  8205  axcaucvglemval  8208  qus0  13941  qusinv  13942  qussub  13943  quscrng  14668