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

Theorem eqeltrri 2542
Description: Substitution of equal classes into membership relation. (Contributed by NM, 21-Jun-1993.)
Hypotheses
Ref Expression
eqeltrr.1
eqeltrr.2
Assertion
Ref Expression
eqeltrri

Proof of Theorem eqeltrri
StepHypRef Expression
1 eqeltrr.1 . . 3
21eqcomi 2470 . 2
3 eqeltrr.2 . 2
42, 3eqeltri 2541 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  e.wcel 1818
This theorem is referenced by:  3eltr3i  2557  zfrep4  4571  p0ex  4639  pp0ex  4641  ord3ex  4642  zfpair  4689  epse  4867  unex  6598  fvresex  6773  abrexex  6774  opabex3  6779  abrexex2  6781  abexssex  6782  abexex  6783  oprabrexex2  6790  seqomlem3  7136  inf0  8059  cantnfOLD  8155  scottexs  8326  kardex  8333  infxpenlem  8412  r1om  8645  cfon  8656  fin23lem16  8736  fin1a2lem6  8806  hsmexlem5  8831  brdom7disj  8930  brdom6disj  8931  1lt2pi  9304  0cn  9609  resubcli  9904  0reALT  9940  1nn  10572  numsucc  11030  nummac  11036  unirnioo  11653  ioorebas  11655  om2uzrani  12063  uzrdg0i  12070  hashunlei  12483  cats1fvn  12823  4sqlem19  14481  dec2dvds  14549  mod2xnegi  14557  modsubi  14558  gcdi  14559  isstruct2  14641  grppropstr  16070  ltbval  18136  funsnfsupOLD  18256  nn0srg  18486  sn0topon  19499  indistop  19503  indisuni  19504  indistps2  19513  indistps2ALT  19515  restbas  19659  leordtval2  19713  iocpnfordt  19716  icomnfordt  19717  iooordt  19718  reordt  19719  dis1stc  20000  ptcmpfi  20314  ustfn  20704  ustn0  20723  retopbas  21267  blssioo  21300  xrtgioo  21311  zcld  21318  cnperf  21325  retopcon  21334  iimulcn  21438  rembl  21951  mbfdm  22035  ismbf  22037  abelthlem9  22835  advlog  23035  advlogexp  23036  cxpcn3  23122  loglesqrt  23132  log2ub  23280  ppi1i  23442  cht2  23446  cht3  23447  bpos1lem  23557  lgslem4  23574  vmadivsum  23667  log2sumbnd  23729  selberg2  23736  selbergr  23753  iscgrg  23904  ishpg  24128  ax5seglem7  24238  usgraexvlem  24395  iseupa  24965  h2hva  25891  h2hsm  25892  h2hnm  25893  norm-ii-i  26054  hhshsslem2  26184  shincli  26280  chincli  26378  lnophdi  26921  imaelshi  26977  rnelshi  26978  bdophdi  27016  nn0omnd  27831  nn0archi  27833  rmulccn  27910  rrhre  27999  sigaex  28109  br2base  28240  sxbrsigalem3  28243  afsval  28551  kur14lem7  28656  retopscon  28694  hfuni  29841  onint1  29914  0mbf  30060  dvtanlem  30064  bddiblnc  30085  ftc1cnnc  30089  neibastop2lem  30178  cncfres  30261  areaquad  31184  sblpnf  31190  lhe4.4ex1a  31234  fourierdlem62  31951  fourierdlem76  31965  usgfis  32446  usgfisALT  32450  lineset  35462  lautset  35806  pautsetN  35822  tendoset  36485
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-cleq 2449  df-clel 2452
  Copyright terms: Public domain W3C validator