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

Theorem eleqtrri 2193
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 2121 . 2  |-  B  =  C
41, 3eleqtri 2192 1  |-  A  e.  C
Colors of variables: wff set class
Syntax hints:    = 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:  3eltr4i  2199  undifexmid  4087  opi1  4124  opi2  4125  ordpwsucexmid  4455  peano1  4478  acexmidlemcase  5737  acexmidlem2  5739  0lt2o  6306  1lt2o  6307  0elixp  6591  ac6sfi  6760  ctssdccl  6964  exmidomni  6982  infnninf  6990  nnnninf  6991  exmidonfinlem  7017  exmidfodomrlemr  7026  exmidfodomrlemrALT  7027  exmidaclem  7032  1lt2pi  7116  prarloclemarch2  7195  prarloclemlt  7269  prarloclemcalc  7278  suplocexprlemdisj  7496  suplocexprlemub  7499  pnfxr  7786  mnfxr  7790  dveflem  12782
  Copyright terms: Public domain W3C validator