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

Theorem eqeltrri 2354
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 2287 . 2  |-  B  =  A
3 eqeltrr.2 . 2  |-  A  e.  C
42, 3eqeltri 2353 1  |-  B  e.  C
Colors of variables: wff set class
Syntax hints:    = wceq 1623    e. wcel 1684
This theorem is referenced by:  3eltr3i  2361  zfrep4  4139  p0ex  4197  pp0ex  4199  ord3ex  4200  zfpair  4212  epse  4376  unex  4518  fvresex  5762  abrexex  5763  opabex3  5769  abrexex2  5780  abexssex  5781  abexex  5782  oprabrexex2  5963  seqomlem3  6464  inf0  7322  cantnf  7395  scottexs  7557  kardex  7564  infxpenlem  7641  r1om  7870  cfon  7881  fin23lem16  7961  fin1a2lem6  8031  hsmexlem5  8056  brdom7disj  8156  brdom6disj  8157  1lt2pi  8529  0cn  8831  resubcli  9109  0reALT  9143  1nn  9757  numsucc  10150  nummac  10156  unirnioo  10743  ioorebas  10745  om2uzrani  11015  uzrdg0i  11022  hashunlei  11377  cats1fvn  11508  4sqlem19  13010  dec2dvds  13078  mod2xnegi  13086  modsubi  13087  gcdi  13088  isstruct2  13157  grppropstr  14502  ltbval  16213  sn0topon  16735  indistop  16739  indisuni  16740  indistps2  16749  indistps2ALT  16751  restbas  16889  leordtval2  16942  iocpnfordt  16945  icomnfordt  16946  iooordt  16947  reordt  16948  dis1stc  17225  ptcmpfi  17504  retopbas  18269  blssioo  18301  xrtgioo  18312  zcld  18319  cnperf  18325  retopcon  18334  iimulcn  18436  rembl  18898  mbfdm  18983  ismbf  18985  abelthlem9  19816  advlog  20001  advlogexp  20002  cxpcn3  20088  loglesqr  20098  log2ub  20245  ppi1i  20406  cht2  20410  cht3  20411  bpos1lem  20521  lgslem4  20538  vmadivsum  20631  log2sumbnd  20693  selberg2  20700  selbergr  20717  h2hva  21554  h2hsm  21555  h2hnm  21556  norm-ii-i  21716  hhshsslem2  21845  shincli  21941  chincli  22039  lnophdi  22582  imaelshi  22638  rnelshi  22639  bdophdi  22677  rmulccn  23301  pnfneige0  23374  br2base  23574  kur14lem7  23743  retopscon  23780  iseupa  23881  ax5seglem7  24563  hfuni  24814  onint1  24888  isrocatset  25957  neibastop2lem  26309  cncfres  26485  funsnfsup  26762  sblpnf  27539  lhe4.4ex1a  27546  usgraexvlem  28127  lineset  29927  lautset  30271  pautsetN  30287  tendoset  30948
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-cleq 2276  df-clel 2279
  Copyright terms: Public domain W3C validator