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

Theorem eceq1d 6078
Description: Equality theorem for equivalence class (deduction form). (Contributed by Jim Kingdon, 31-Dec-2019.)
Hypothesis
Ref Expression
eceq1d.1 (φA = B)
Assertion
Ref Expression
eceq1d (φ → [A]𝐶 = [B]𝐶)

Proof of Theorem eceq1d
StepHypRef Expression
1 eceq1d.1 . 2 (φA = B)
2 eceq1 6077 . 2 (A = B → [A]𝐶 = [B]𝐶)
31, 2syl 14 1 (φ → [A]𝐶 = [B]𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1242  [cec 6040
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-sn 3373  df-pr 3374  df-op 3376  df-br 3756  df-opab 3810  df-xp 4294  df-cnv 4296  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-ec 6044
This theorem is referenced by:  brecop  6132  eroveu  6133  th3qlem1  6144  th3qlem2  6145  th3q  6147  oviec  6148  ecovcom  6149  ecovicom  6150  ecovass  6151  ecoviass  6152  ecovdi  6153  ecovidi  6154  mulidnq  6373  recexnq  6374  ltexnqq  6391  archnqq  6400  prarloclemarch2  6402  addnq0mo  6430  mulnq0mo  6431  addnnnq0  6432  mulnnnq0  6433  nqnq0a  6437  nqnq0m  6438  nq0a0  6440  nnanq0  6441  distrnq0  6442  mulcomnq0  6443  addassnq0  6445  addpinq1  6447  nq02m  6448  prarloclemlo  6477  prarloclem3  6480  prarloclem5  6483  caucvgprlemnkj  6637  caucvgprlemnbj  6638  caucvgprlemm  6639  caucvgprlemdisj  6645  caucvgprlemloc  6646  caucvgprlemcl  6647  caucvgprlemladdfu  6648  caucvgprlemladdrl  6649  caucvgprlem1  6650  caucvgprlem2  6651  caucvgpr  6653  addsrmo  6671  mulsrmo  6672  addsrpr  6673  mulsrpr  6674  pitonnlem2  6743  pitonn  6744
  Copyright terms: Public domain W3C validator