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

Theorem eleqtrri 2213
Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
eleqtrr.1  |-  A  e.  B
eleqtrr.2  |-  C  =  B
Assertion
Ref Expression
eleqtrri  |-  A  e.  C

Proof of Theorem eleqtrri
StepHypRef Expression
1 eleqtrr.1 . 2  |-  A  e.  B
2 eleqtrr.2 . . 3  |-  C  =  B
32eqcomi 2141 . 2  |-  B  =  C
41, 3eleqtri 2212 1  |-  A  e.  C
Colors of variables: wff set class
Syntax hints:    = wceq 1331    e. wcel 1480
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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2119
This theorem depends on definitions:  df-bi 116  df-cleq 2130  df-clel 2133
This theorem is referenced by:  3eltr4i  2219  undifexmid  4112  opi1  4149  opi2  4150  ordpwsucexmid  4480  peano1  4503  acexmidlemcase  5762  acexmidlem2  5764  0lt2o  6331  1lt2o  6332  0elixp  6616  ac6sfi  6785  ctssdccl  6989  exmidomni  7007  infnninf  7015  nnnninf  7016  exmidonfinlem  7042  exmidfodomrlemr  7051  exmidfodomrlemrALT  7052  exmidaclem  7057  1lt2pi  7141  prarloclemarch2  7220  prarloclemlt  7294  prarloclemcalc  7303  suplocexprlemdisj  7521  suplocexprlemub  7524  pnfxr  7811  mnfxr  7815  dveflem  12844
  Copyright terms: Public domain W3C validator