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

Theorem eleqtrri 2160
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 2089 . 2  |-  B  =  C
41, 3eleqtri 2159 1  |-  A  e.  C
Colors of variables: wff set class
Syntax hints:    = wceq 1287    e. wcel 1436
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 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-17 1462  ax-ial 1470  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078  df-clel 2081
This theorem is referenced by:  3eltr4i  2166  undifexmid  3995  opi1  4026  opi2  4027  ordpwsucexmid  4352  peano1  4375  acexmidlemcase  5589  acexmidlem2  5591  ac6sfi  6547  djuun  6681  exmidomni  6719  fodjuomnilemf  6721  infnninf  6726  nnnninf  6727  exmidfodomrlemr  6749  exmidfodomrlemrALT  6750  1lt2pi  6820  prarloclemarch2  6899  prarloclemlt  6973  prarloclemcalc  6982  pnfxr  7461  mnfxr  7465  0lt2o  11242  1lt2o  11243
  Copyright terms: Public domain W3C validator