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

Theorem eqeltrri 2507
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 2440 . 2  |-  B  =  A
3 eqeltrr.2 . 2  |-  A  e.  C
42, 3eqeltri 2506 1  |-  B  e.  C
Colors of variables: wff set class
Syntax hints:    = wceq 1652    e. wcel 1725
This theorem is referenced by:  3eltr3i  2514  zfrep4  4328  p0ex  4386  pp0ex  4388  ord3ex  4389  zfpair  4401  epse  4565  unex  4707  fvresex  5982  abrexex  5983  opabex3  5990  abrexex2  6001  abexssex  6002  abexex  6003  oprabrexex2  6189  seqomlem3  6709  inf0  7576  cantnf  7649  scottexs  7811  kardex  7818  infxpenlem  7895  r1om  8124  cfon  8135  fin23lem16  8215  fin1a2lem6  8285  hsmexlem5  8310  brdom7disj  8409  brdom6disj  8410  1lt2pi  8782  0cn  9084  resubcli  9363  0reALT  9397  1nn  10011  numsucc  10408  nummac  10414  unirnioo  11004  ioorebas  11006  om2uzrani  11292  uzrdg0i  11299  hashunlei  11684  cats1fvn  11822  4sqlem19  13331  dec2dvds  13399  mod2xnegi  13407  modsubi  13408  gcdi  13409  isstruct2  13478  grppropstr  14825  ltbval  16532  sn0topon  17062  indistop  17066  indisuni  17067  indistps2  17076  indistps2ALT  17078  restbas  17222  leordtval2  17276  iocpnfordt  17279  icomnfordt  17280  iooordt  17281  reordt  17282  dis1stc  17562  ptcmpfi  17845  ustfn  18231  ustn0  18250  retopbas  18794  blssioo  18826  xrtgioo  18837  zcld  18844  cnperf  18851  retopcon  18860  iimulcn  18963  rembl  19435  mbfdm  19520  ismbf  19522  abelthlem9  20356  advlog  20545  advlogexp  20546  cxpcn3  20632  loglesqr  20642  log2ub  20789  ppi1i  20951  cht2  20955  cht3  20956  bpos1lem  21066  lgslem4  21083  vmadivsum  21176  log2sumbnd  21238  selberg2  21245  selbergr  21262  usgraexvlem  21414  iseupa  21687  h2hva  22477  h2hsm  22478  h2hnm  22479  norm-ii-i  22639  hhshsslem2  22768  shincli  22864  chincli  22962  lnophdi  23505  imaelshi  23561  rnelshi  23562  bdophdi  23600  rmulccn  24314  rrhre  24387  sigaex  24492  br2base  24619  sxbrsigalem3  24622  sitgclre  24659  sitmcl  24663  kur14lem7  24898  retopscon  24936  ax5seglem7  25874  hfuni  26125  onint1  26199  0mbf  26252  bddiblnc  26275  ftc1cnnc  26279  neibastop2lem  26389  cncfres  26474  funsnfsup  26743  sblpnf  27516  lhe4.4ex1a  27523  lineset  30535  lautset  30879  pautsetN  30895  tendoset  31556
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2429  df-clel 2432
  Copyright terms: Public domain W3C validator