Theorem eceq1d 6549

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

Hypothesis

Ref	Expression
eceq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
eceq1d	|- ( ph -> [ A ] C = [ B ] C )

Proof of Theorem eceq1d

Step	Hyp	Ref	Expression
1		eceq1d.1	. 2 |- ( ph -> A = B )
2		eceq1 6548	. 2 |- ( A = B -> [ A ] C = [ B ] C )
3	1, 2	syl 14	1 |- ( ph -> [ A ] C = [ B ] C )

Syntax hints:   -> wi 4   = wceq 1348   [cec 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125  df-in 3127  df-ss 3134  df-sn 3589  df-pr 3590  df-op 3592  df-br 3990  df-opab 4051  df-xp 4617  df-cnv 4619  df-dm 4621  df-rn 4622  df-res 4623  df-ima 4624  df-ec 6515

This theorem is referenced by:  brecop  6603  eroveu  6604  th3qlem1  6615  th3qlem2  6616  th3q  6618  oviec  6619  ecovcom  6620  ecovicom  6621  ecovass  6622  ecoviass  6623  ecovdi  6624  ecovidi  6625  mulidnq  7351  recexnq  7352  ltexnqq  7370  archnqq  7379  prarloclemarch2  7381  addnq0mo  7409  mulnq0mo  7410  addnnnq0  7411  mulnnnq0  7412  nqnq0a  7416  nqnq0m  7417  nq0a0  7419  nnanq0  7420  distrnq0  7421  mulcomnq0  7422  addassnq0  7424  addpinq1  7426  nq02m  7427  prarloclemlo  7456  prarloclem3  7459  prarloclem5  7462  caucvgprlemnkj  7628  caucvgprlemnbj  7629  caucvgprlemm  7630  caucvgprlemdisj  7636  caucvgprlemloc  7637  caucvgprlemcl  7638  caucvgprlemladdfu  7639  caucvgprlemladdrl  7640  caucvgprlem1  7641  caucvgprlem2  7642  caucvgpr  7644  caucvgprprlemell  7647  caucvgprprlemelu  7648  caucvgprprlemcbv  7649  caucvgprprlemval  7650  caucvgprprlemnkeqj  7652  caucvgprprlemmu  7657  caucvgprprlemopl  7659  caucvgprprlemlol  7660  caucvgprprlemopu  7661  caucvgprprlemloc  7665  caucvgprprlemclphr  7667  caucvgprprlemexbt  7668  caucvgprprlem1  7671  caucvgprprlem2  7672  addsrmo  7705  mulsrmo  7706  addsrpr  7707  mulsrpr  7708  prsrriota  7750  caucvgsrlemfv  7753  caucvgsr  7764  suplocsrlemb  7768  suplocsrlempr  7769  suplocsrlem  7770  suplocsr  7771  pitonnlem2  7809  pitonn  7810  nntopi  7856  axcaucvglemval  7859