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

Theorem eleqtrd 2194
Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
Hypotheses
Ref Expression
eleqtrd.1  |-  ( ph  ->  A  e.  B )
eleqtrd.2  |-  ( ph  ->  B  =  C )
Assertion
Ref Expression
eleqtrd  |-  ( ph  ->  A  e.  C )

Proof of Theorem eleqtrd
StepHypRef Expression
1 eleqtrd.1 . 2  |-  ( ph  ->  A  e.  B )
2 eleqtrd.2 . . 3  |-  ( ph  ->  B  =  C )
32eleq2d 2185 . 2  |-  ( ph  ->  ( A  e.  B  <->  A  e.  C ) )
41, 3mpbid 146 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1314    e. wcel 1463
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-5 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-cleq 2108  df-clel 2111
This theorem is referenced by:  eleqtrrd  2195  3eltr3d  2198  eleqtrid  2204  syl6eleq  2208  opth1  4126  0nelop  4138  tfisi  4469  ercl  6406  erth  6439  ecelqsdm  6465  phpm  6725  suplocexprlemmu  7490  suplocexprlemloc  7493  lincmb01cmp  9726  fzopth  9781  fzoaddel2  9910  fzosubel2  9912  fzocatel  9916  zpnn0elfzo1  9925  fzoend  9939  peano2fzor  9949  monoord2  10190  ser3mono  10191  bcpasc  10452  zfz1isolemiso  10522  fisum0diag2  11156  isumsplit  11200  iscnp4  12282  cnrest2r  12301  txbasval  12331  txlm  12343  xmetunirn  12422  xblss2ps  12468  blbas  12497  mopntopon  12507  isxms2  12516  metcnpi  12579  metcnpi2  12580  tgioo  12610  cncfmpt2fcntop  12649  limccl  12680  limcimolemlt  12685  limccnp2cntop  12698  dvmulxxbr  12718  dvcoapbr  12723  dvcjbr  12724  dvrecap  12729
  Copyright terms: Public domain W3C validator