Theorem eceq1d 6729

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

Syntax hints:   → wi 4   = wceq 1395  [cec 6691

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-sn 3672  df-pr 3673  df-op 3675  df-br 4084  df-opab 4146  df-xp 4726  df-cnv 4728  df-dm 4730  df-rn 4731  df-res 4732  df-ima 4733  df-ec 6695

This theorem is referenced by:  brecop  6785  eroveu  6786  th3qlem1  6797  th3qlem2  6798  th3q  6800  oviec  6801  ecovcom  6802  ecovicom  6803  ecovass  6804  ecoviass  6805  ecovdi  6806  ecovidi  6807  mulidnq  7592  recexnq  7593  ltexnqq  7611  archnqq  7620  prarloclemarch2  7622  addnq0mo  7650  mulnq0mo  7651  addnnnq0  7652  mulnnnq0  7653  nqnq0a  7657  nqnq0m  7658  nq0a0  7660  nnanq0  7661  distrnq0  7662  mulcomnq0  7663  addassnq0  7665  addpinq1  7667  nq02m  7668  prarloclemlo  7697  prarloclem3  7700  prarloclem5  7703  caucvgprlemnkj  7869  caucvgprlemnbj  7870  caucvgprlemm  7871  caucvgprlemdisj  7877  caucvgprlemloc  7878  caucvgprlemcl  7879  caucvgprlemladdfu  7880  caucvgprlemladdrl  7881  caucvgprlem1  7882  caucvgprlem2  7883  caucvgpr  7885  caucvgprprlemell  7888  caucvgprprlemelu  7889  caucvgprprlemcbv  7890  caucvgprprlemval  7891  caucvgprprlemnkeqj  7893  caucvgprprlemmu  7898  caucvgprprlemopl  7900  caucvgprprlemlol  7901  caucvgprprlemopu  7902  caucvgprprlemloc  7906  caucvgprprlemclphr  7908  caucvgprprlemexbt  7909  caucvgprprlem1  7912  caucvgprprlem2  7913  addsrmo  7946  mulsrmo  7947  addsrpr  7948  mulsrpr  7949  prsrriota  7991  caucvgsrlemfv  7994  caucvgsr  8005  suplocsrlemb  8009  suplocsrlempr  8010  suplocsrlem  8011  suplocsr  8012  pitonnlem2  8050  pitonn  8051  nntopi  8097  axcaucvglemval  8100  qus0  13793  qusinv  13794  qussub  13795  quscrng  14518