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

Theorem eleqtrri 2163
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 2092 . 2  |-  B  =  C
41, 3eleqtri 2162 1  |-  A  e.  C
Colors of variables: wff set class
Syntax hints:    = wceq 1289    e. wcel 1438
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-cleq 2081  df-clel 2084
This theorem is referenced by:  3eltr4i  2169  undifexmid  4019  opi1  4050  opi2  4051  ordpwsucexmid  4376  peano1  4399  acexmidlemcase  5629  acexmidlem2  5631  ac6sfi  6594  djuun  6739  exmidomni  6777  fodjuomnilemf  6779  infnninf  6784  nnnninf  6785  exmidfodomrlemr  6807  exmidfodomrlemrALT  6808  1lt2pi  6878  prarloclemarch2  6957  prarloclemlt  7031  prarloclemcalc  7040  pnfxr  7519  mnfxr  7523  0lt2o  11531  1lt2o  11532
  Copyright terms: Public domain W3C validator