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

Theorem eleqtrri 2216
 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 2144 . 2 𝐵 = 𝐶
41, 3eleqtri 2215 1 𝐴𝐶
 Colors of variables: wff set class Syntax hints:   = wceq 1332   ∈ wcel 1481 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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-ext 2122 This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-clel 2136 This theorem is referenced by:  3eltr4i  2222  undifexmid  4125  opi1  4162  opi2  4163  ordpwsucexmid  4493  peano1  4516  acexmidlemcase  5777  acexmidlem2  5779  0lt2o  6346  1lt2o  6347  0elixp  6631  ac6sfi  6800  ctssdccl  7004  exmidomni  7022  infnninf  7030  nnnninf  7031  exmidonfinlem  7066  exmidfodomrlemr  7075  exmidfodomrlemrALT  7076  exmidaclem  7081  1lt2pi  7172  prarloclemarch2  7251  prarloclemlt  7325  prarloclemcalc  7334  suplocexprlemdisj  7552  suplocexprlemub  7555  pnfxr  7842  mnfxr  7846  dveflem  12895
 Copyright terms: Public domain W3C validator