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

Theorem eqeltrri 2111
 Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
eqeltrr.1
eqeltrr.2
Assertion
Ref Expression
eqeltrri

Proof of Theorem eqeltrri
StepHypRef Expression
1 eqeltrr.1 . . 3
21eqcomi 2044 . 2
3 eqeltrr.2 . 2
42, 3eqeltri 2110 1
 Colors of variables: wff set class Syntax hints:   wceq 1243   wcel 1393 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022 This theorem depends on definitions:  df-bi 110  df-cleq 2033  df-clel 2036 This theorem is referenced by:  3eltr3i  2118  p0ex  3939  epse  4079  unex  4176  ordtri2orexmid  4248  onsucsssucexmid  4252  ordsoexmid  4286  ordtri2or2exmid  4296  nnregexmid  4342  abrexex  5744  opabex3  5749  abrexex2  5751  abexssex  5752  abexex  5753  oprabrexex2  5757  tfr0  5937  1lt2pi  6438  prarloclemarch2  6517  prarloclemlt  6591  0cn  7019  resubcli  7274  0reALT  7308  numsucc  8393  nummac  8399  qreccl  8576  unirnioo  8842  bj-unex  10039
 Copyright terms: Public domain W3C validator