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

Theorem eceq1d 6433
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
StepHypRef Expression
1 eceq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 eceq1 6432 . 2  |-  ( A  =  B  ->  [ A ] C  =  [ B ] C )
31, 2syl 14 1  |-  ( ph  ->  [ A ] C  =  [ B ] C
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1316   [cec 6395
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 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-3an 949  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-v 2662  df-un 3045  df-in 3047  df-ss 3054  df-sn 3503  df-pr 3504  df-op 3506  df-br 3900  df-opab 3960  df-xp 4515  df-cnv 4517  df-dm 4519  df-rn 4520  df-res 4521  df-ima 4522  df-ec 6399
This theorem is referenced by:  brecop  6487  eroveu  6488  th3qlem1  6499  th3qlem2  6500  th3q  6502  oviec  6503  ecovcom  6504  ecovicom  6505  ecovass  6506  ecoviass  6507  ecovdi  6508  ecovidi  6509  mulidnq  7165  recexnq  7166  ltexnqq  7184  archnqq  7193  prarloclemarch2  7195  addnq0mo  7223  mulnq0mo  7224  addnnnq0  7225  mulnnnq0  7226  nqnq0a  7230  nqnq0m  7231  nq0a0  7233  nnanq0  7234  distrnq0  7235  mulcomnq0  7236  addassnq0  7238  addpinq1  7240  nq02m  7241  prarloclemlo  7270  prarloclem3  7273  prarloclem5  7276  caucvgprlemnkj  7442  caucvgprlemnbj  7443  caucvgprlemm  7444  caucvgprlemdisj  7450  caucvgprlemloc  7451  caucvgprlemcl  7452  caucvgprlemladdfu  7453  caucvgprlemladdrl  7454  caucvgprlem1  7455  caucvgprlem2  7456  caucvgpr  7458  caucvgprprlemell  7461  caucvgprprlemelu  7462  caucvgprprlemcbv  7463  caucvgprprlemval  7464  caucvgprprlemnkeqj  7466  caucvgprprlemmu  7471  caucvgprprlemopl  7473  caucvgprprlemlol  7474  caucvgprprlemopu  7475  caucvgprprlemloc  7479  caucvgprprlemclphr  7481  caucvgprprlemexbt  7482  caucvgprprlem1  7485  caucvgprprlem2  7486  addsrmo  7519  mulsrmo  7520  addsrpr  7521  mulsrpr  7522  prsrriota  7564  caucvgsrlemfv  7567  caucvgsr  7578  suplocsrlemb  7582  suplocsrlempr  7583  suplocsrlem  7584  suplocsr  7585  pitonnlem2  7623  pitonn  7624  nntopi  7670  axcaucvglemval  7673
  Copyright terms: Public domain W3C validator