MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqeltrri Unicode version

Theorem eqeltrri 2475
Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
eqeltrr.1  |-  A  =  B
eqeltrr.2  |-  A  e.  C
Assertion
Ref Expression
eqeltrri  |-  B  e.  C

Proof of Theorem eqeltrri
StepHypRef Expression
1 eqeltrr.1 . . 3  |-  A  =  B
21eqcomi 2408 . 2  |-  B  =  A
3 eqeltrr.2 . 2  |-  A  e.  C
42, 3eqeltri 2474 1  |-  B  e.  C
Colors of variables: wff set class
Syntax hints:    = wceq 1649    e. wcel 1721
This theorem is referenced by:  3eltr3i  2482  zfrep4  4288  p0ex  4346  pp0ex  4348  ord3ex  4349  zfpair  4361  epse  4525  unex  4666  fvresex  5941  abrexex  5942  opabex3  5949  abrexex2  5960  abexssex  5961  abexex  5962  oprabrexex2  6148  seqomlem3  6668  inf0  7532  cantnf  7605  scottexs  7767  kardex  7774  infxpenlem  7851  r1om  8080  cfon  8091  fin23lem16  8171  fin1a2lem6  8241  hsmexlem5  8266  brdom7disj  8365  brdom6disj  8366  1lt2pi  8738  0cn  9040  resubcli  9319  0reALT  9353  1nn  9967  numsucc  10364  nummac  10370  unirnioo  10960  ioorebas  10962  om2uzrani  11247  uzrdg0i  11254  hashunlei  11639  cats1fvn  11777  4sqlem19  13286  dec2dvds  13354  mod2xnegi  13362  modsubi  13363  gcdi  13364  isstruct2  13433  grppropstr  14780  ltbval  16487  sn0topon  17017  indistop  17021  indisuni  17022  indistps2  17031  indistps2ALT  17033  restbas  17176  leordtval2  17230  iocpnfordt  17233  icomnfordt  17234  iooordt  17235  reordt  17236  dis1stc  17515  ptcmpfi  17798  ustfn  18184  ustn0  18203  retopbas  18747  blssioo  18779  xrtgioo  18790  zcld  18797  cnperf  18804  retopcon  18813  iimulcn  18916  rembl  19388  mbfdm  19473  ismbf  19475  abelthlem9  20309  advlog  20498  advlogexp  20499  cxpcn3  20585  loglesqr  20595  log2ub  20742  ppi1i  20904  cht2  20908  cht3  20909  bpos1lem  21019  lgslem4  21036  vmadivsum  21129  log2sumbnd  21191  selberg2  21198  selbergr  21215  usgraexvlem  21367  iseupa  21640  h2hva  22430  h2hsm  22431  h2hnm  22432  norm-ii-i  22592  hhshsslem2  22721  shincli  22817  chincli  22915  lnophdi  23458  imaelshi  23514  rnelshi  23515  bdophdi  23553  rmulccn  24267  rrhre  24340  sigaex  24445  br2base  24572  sxbrsigalem3  24575  sitgclre  24612  sitmcl  24616  kur14lem7  24851  retopscon  24889  ax5seglem7  25778  hfuni  26029  onint1  26103  0mbf  26151  bddiblnc  26174  ftc1cnnc  26178  neibastop2lem  26279  cncfres  26364  funsnfsup  26633  sblpnf  27407  lhe4.4ex1a  27414  lineset  30220  lautset  30564  pautsetN  30580  tendoset  31241
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2397  df-clel 2400
  Copyright terms: Public domain W3C validator