ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eceq1d GIF version

Theorem eceq1d 6208
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
StepHypRef Expression
1 eceq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 eceq1 6207 . 2 (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶)
31, 2syl 14 1 (𝜑 → [𝐴]𝐶 = [𝐵]𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1285  [cec 6170
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-v 2604  df-un 2978  df-in 2980  df-ss 2987  df-sn 3412  df-pr 3413  df-op 3415  df-br 3794  df-opab 3848  df-xp 4377  df-cnv 4379  df-dm 4381  df-rn 4382  df-res 4383  df-ima 4384  df-ec 6174
This theorem is referenced by:  brecop  6262  eroveu  6263  th3qlem1  6274  th3qlem2  6275  th3q  6277  oviec  6278  ecovcom  6279  ecovicom  6280  ecovass  6281  ecoviass  6282  ecovdi  6283  ecovidi  6284  mulidnq  6641  recexnq  6642  ltexnqq  6660  archnqq  6669  prarloclemarch2  6671  addnq0mo  6699  mulnq0mo  6700  addnnnq0  6701  mulnnnq0  6702  nqnq0a  6706  nqnq0m  6707  nq0a0  6709  nnanq0  6710  distrnq0  6711  mulcomnq0  6712  addassnq0  6714  addpinq1  6716  nq02m  6717  prarloclemlo  6746  prarloclem3  6749  prarloclem5  6752  caucvgprlemnkj  6918  caucvgprlemnbj  6919  caucvgprlemm  6920  caucvgprlemdisj  6926  caucvgprlemloc  6927  caucvgprlemcl  6928  caucvgprlemladdfu  6929  caucvgprlemladdrl  6930  caucvgprlem1  6931  caucvgprlem2  6932  caucvgpr  6934  caucvgprprlemell  6937  caucvgprprlemelu  6938  caucvgprprlemcbv  6939  caucvgprprlemval  6940  caucvgprprlemnkeqj  6942  caucvgprprlemmu  6947  caucvgprprlemopl  6949  caucvgprprlemlol  6950  caucvgprprlemopu  6951  caucvgprprlemloc  6955  caucvgprprlemclphr  6957  caucvgprprlemexbt  6958  caucvgprprlem1  6961  caucvgprprlem2  6962  addsrmo  6982  mulsrmo  6983  addsrpr  6984  mulsrpr  6985  prsrriota  7026  caucvgsrlemfv  7029  caucvgsr  7040  pitonnlem2  7077  pitonn  7078  nntopi  7122  axcaucvglemval  7125
  Copyright terms: Public domain W3C validator