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

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

Proof of Theorem eqeltrri
StepHypRef Expression
1 eqeltrri.1 . . 3 𝐴 = 𝐵
21eqcomi 2830 . 2 𝐵 = 𝐴
3 eqeltrri.2 . 2 𝐴𝐶
42, 3eqeltri 2909 1 𝐵𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  wcel 2105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814  df-clel 2893
This theorem is referenced by:  3eltr3i  2925  zfrep4  5192  p0ex  5276  pp0ex  5278  ord3ex  5279  zfpair  5313  epse  5532  unex  7457  fvresex  7652  opabex3  7659  abexssex  7662  abexex  7663  oprabrexex2  7670  seqomlem3  8079  inf0  9073  scottexs  9305  kardex  9312  infxpenlem  9428  r1om  9655  cfon  9666  fin23lem16  9746  fin1a2lem6  9816  hsmexlem5  9841  brdom7disj  9942  brdom6disj  9943  1lt2pi  10316  0cn  10622  resubcli  10937  0reALT  10972  1nn  11638  10nn  12103  numsucc  12127  nummac  12132  unirnioo  12827  ioorebas  12829  fz0to4untppr  13000  om2uzrani  13310  uzrdg0i  13317  hashunlei  13776  cats1fvn  14210  trclubi  14346  4sqlem19  16289  dec2dvds  16389  mod2xnegi  16397  modsubi  16398  gcdi  16399  isstruct2  16483  grppropstr  18060  ltbval  20182  nn0srg  20545  sn0topon  21536  indistop  21540  indisuni  21541  indistps2  21550  indistps2ALT  21552  restbas  21696  leordtval2  21750  iocpnfordt  21753  icomnfordt  21754  iooordt  21755  reordt  21756  dis1stc  22037  ptcmpfi  22351  ustfn  22739  ustn0  22758  retopbas  23298  blssioo  23332  xrtgioo  23343  zcld  23350  cnperf  23357  retopconn  23366  iimulcn  23471  rembl  24070  mbfdm  24156  ismbf  24158  mbf0  24164  abelthlem9  24957  advlog  25164  advlogexp  25165  2irrexpq  25240  cxpcn3  25256  loglesqrt  25266  log2ub  25455  ppi1i  25673  cht2  25677  cht3  25678  bpos1lem  25786  lgslem4  25804  vmadivsum  25986  log2sumbnd  26048  selberg2  26055  selbergr  26072  iscgrg  26226  ishpg  26473  ax5seglem7  26649  h2hva  28679  h2hsm  28680  h2hnm  28681  norm-ii-i  28842  hhshsslem2  28973  shincli  29067  chincli  29165  lnophdi  29707  imaelshi  29763  rnelshi  29764  bdophdi  29802  dfdec100  30474  dpadd2  30514  dpmul  30517  dpmul4  30518  nn0omnd  30842  nn0archi  30844  ccfldextrr  30938  lmatfvlem  30980  rmulccn  31071  rrhre  31162  sigaex  31269  br2base  31427  sxbrsigalem3  31430  carsgclctunlem3  31478  sitmcl  31509  rpsqrtcn  31764  hgt750lem  31822  hgt750lem2  31823  afsval  31842  kur14lem7  32357  retopsconn  32394  satfvsuclem1  32504  fmlasuc0  32529  hfuni  33543  neibastop2lem  33606  onint1  33695  topdifinffinlem  34511  poimirlem9  34783  poimirlem28  34802  poimirlem30  34804  poimirlem32  34806  bddiblnc  34844  ftc1cnnc  34848  cncfres  34926  lineset  36756  lautset  37100  pautsetN  37116  tendoset  37777  decpmulnc  39053  decpmul  39054  areaquad  39703  sblpnf  40522  lhe4.4ex1a  40541  fourierdlem62  42334  fourierdlem76  42348  65537prm  43585  11gbo  43787  bgoldbtbndlem1  43817
  Copyright terms: Public domain W3C validator