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

Theorem eleqtrd 2196
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 2187 . 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 1316    e. wcel 1465
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 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-17 1491  ax-ial 1499  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110  df-clel 2113
This theorem is referenced by:  eleqtrrd  2197  3eltr3d  2200  eleqtrid  2206  eleqtrdi  2210  opth1  4128  0nelop  4140  tfisi  4471  ercl  6408  erth  6441  ecelqsdm  6467  phpm  6727  suplocexprlemmu  7494  suplocexprlemloc  7497  lincmb01cmp  9754  fzopth  9809  fzoaddel2  9938  fzosubel2  9940  fzocatel  9944  zpnn0elfzo1  9953  fzoend  9967  peano2fzor  9977  monoord2  10218  ser3mono  10219  bcpasc  10480  zfz1isolemiso  10550  fisum0diag2  11184  isumsplit  11228  iscnp4  12314  cnrest2r  12333  txbasval  12363  txlm  12375  xmetunirn  12454  xblss2ps  12500  blbas  12529  mopntopon  12539  isxms2  12548  metcnpi  12611  metcnpi2  12612  tgioo  12642  cncfmpt2fcntop  12681  limccl  12724  limcimolemlt  12729  limccnp2cntop  12742  dvmulxxbr  12762  dvcoapbr  12767  dvcjbr  12768  dvrecap  12773
  Copyright terms: Public domain W3C validator