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

Theorem eqeltrri 2387
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 2320 . 2  |-  B  =  A
3 eqeltrr.2 . 2  |-  A  e.  C
42, 3eqeltri 2386 1  |-  B  e.  C
Colors of variables: wff set class
Syntax hints:    = wceq 1633    e. wcel 1701
This theorem is referenced by:  3eltr3i  2394  zfrep4  4176  p0ex  4234  pp0ex  4236  ord3ex  4237  zfpair  4249  epse  4413  unex  4555  fvresex  5803  abrexex  5804  opabex3  5811  abrexex2  5822  abexssex  5823  abexex  5824  oprabrexex2  6005  seqomlem3  6506  inf0  7367  cantnf  7440  scottexs  7602  kardex  7609  infxpenlem  7686  r1om  7915  cfon  7926  fin23lem16  8006  fin1a2lem6  8076  hsmexlem5  8101  brdom7disj  8201  brdom6disj  8202  1lt2pi  8574  0cn  8876  resubcli  9154  0reALT  9188  1nn  9802  numsucc  10197  nummac  10203  unirnioo  10790  ioorebas  10792  om2uzrani  11062  uzrdg0i  11069  hashunlei  11424  cats1fvn  11555  4sqlem19  13057  dec2dvds  13125  mod2xnegi  13133  modsubi  13134  gcdi  13135  isstruct2  13204  grppropstr  14551  ltbval  16262  sn0topon  16791  indistop  16795  indisuni  16796  indistps2  16805  indistps2ALT  16807  restbas  16945  leordtval2  16998  iocpnfordt  17001  icomnfordt  17002  iooordt  17003  reordt  17004  dis1stc  17281  ptcmpfi  17560  retopbas  18321  blssioo  18353  xrtgioo  18364  zcld  18371  cnperf  18377  retopcon  18386  iimulcn  18489  rembl  18951  mbfdm  19036  ismbf  19038  abelthlem9  19869  advlog  20054  advlogexp  20055  cxpcn3  20141  loglesqr  20151  log2ub  20298  ppi1i  20459  cht2  20463  cht3  20464  bpos1lem  20574  lgslem4  20591  vmadivsum  20684  log2sumbnd  20746  selberg2  20753  selbergr  20770  h2hva  21609  h2hsm  21610  h2hnm  21611  norm-ii-i  21771  hhshsslem2  21900  shincli  21996  chincli  22094  lnophdi  22637  imaelshi  22693  rnelshi  22694  bdophdi  22732  rmulccn  23383  pnfneige0  23405  ustfn  23418  ustn0  23433  br2base  23793  sxbrsigalem3  23796  sxbrsiga  23814  kur14lem7  24027  retopscon  24064  iseupa  24165  ax5seglem7  24949  hfuni  25200  onint1  25274  bddiblnc  25335  ftc1cnnc  25339  neibastop2lem  25458  cncfres  25633  funsnfsup  25910  sblpnf  26687  lhe4.4ex1a  26694  usgraexvlem  27360  lineset  29745  lautset  30089  pautsetN  30105  tendoset  30766
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-11 1732  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1533  df-cleq 2309  df-clel 2312
  Copyright terms: Public domain W3C validator