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

Theorem eqeltrri 2127
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 2060 . 2 𝐵 = 𝐴
3 eqeltrr.2 . 2 𝐴𝐶
42, 3eqeltri 2126 1 𝐵𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1259  wcel 1409
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049  df-clel 2052
This theorem is referenced by:  3eltr3i  2134  p0ex  3967  epse  4107  unex  4204  ordtri2orexmid  4276  onsucsssucexmid  4280  ordsoexmid  4314  ordtri2or2exmid  4324  nnregexmid  4370  abrexex  5772  opabex3  5777  abrexex2  5779  abexssex  5780  abexex  5781  oprabrexex2  5785  tfr0  5968  1lt2pi  6496  prarloclemarch2  6575  prarloclemlt  6649  0cn  7077  resubcli  7337  0reALT  7371  10nn  8442  numsucc  8466  nummac  8471  qreccl  8674  unirnioo  8943  bj-unex  10426
  Copyright terms: Public domain W3C validator