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

Theorem eleqtrri 2170
Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
eleqtrr.1 𝐴𝐵
eleqtrr.2 𝐶 = 𝐵
Assertion
Ref Expression
eleqtrri 𝐴𝐶

Proof of Theorem eleqtrri
StepHypRef Expression
1 eleqtrr.1 . 2 𝐴𝐵
2 eleqtrr.2 . . 3 𝐶 = 𝐵
32eqcomi 2099 . 2 𝐵 = 𝐶
41, 3eleqtri 2169 1 𝐴𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1296  wcel 1445
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-4 1452  ax-17 1471  ax-ial 1479  ax-ext 2077
This theorem depends on definitions:  df-bi 116  df-cleq 2088  df-clel 2091
This theorem is referenced by:  3eltr4i  2176  undifexmid  4049  opi1  4083  opi2  4084  ordpwsucexmid  4414  peano1  4437  acexmidlemcase  5685  acexmidlem2  5687  0lt2o  6243  1lt2o  6244  0elixp  6526  ac6sfi  6694  djuun  6840  exmidomni  6885  infnninf  6893  nnnninf  6894  exmidfodomrlemr  6925  exmidfodomrlemrALT  6926  1lt2pi  6996  prarloclemarch2  7075  prarloclemlt  7149  prarloclemcalc  7158  pnfxr  7637  mnfxr  7641
  Copyright terms: Public domain W3C validator