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

Theorem eqeltrri 2213
 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 2143 . 2 𝐵 = 𝐴
3 eqeltrr.2 . 2 𝐴𝐶
42, 3eqeltri 2212 1 𝐵𝐶
 Colors of variables: wff set class Syntax hints:   = wceq 1331   ∈ wcel 1480 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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121 This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135 This theorem is referenced by:  3eltr3i  2220  p0ex  4112  epse  4264  unex  4362  ordtri2orexmid  4438  onsucsssucexmid  4442  ordsoexmid  4477  ordtri2or2exmid  4486  nnregexmid  4534  abrexex  6015  opabex3  6020  abrexex2  6022  abexssex  6023  abexex  6024  oprabrexex2  6028  tfr0dm  6219  exmidonfinlem  7049  1lt2pi  7155  prarloclemarch2  7234  prarloclemlt  7308  0cn  7765  resubcli  8032  0reALT  8066  10nn  9204  numsucc  9228  nummac  9233  qreccl  9441  unirnioo  9763  sn0topon  12267  retopbas  12702  blssioo  12724  bj-unex  13147  nninffeq  13246  exmidsbthrlem  13247
 Copyright terms: Public domain W3C validator