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

Theorem eqeltrri 2835
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 2745 . 2 𝐵 = 𝐴
3 eqeltrri.2 . 2 𝐴𝐶
42, 3eqeltri 2834 1 𝐵𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1541  wcel 2106
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2728  df-clel 2814
This theorem is referenced by:  3eltr3i  2850  zfrep4  5253  p0ex  5339  pp0ex  5341  ord3ex  5342  zfpair  5376  epse  5616  unex  7679  fvresex  7891  opabex3  7899  abexssex  7902  abexex  7903  oprabrexex2  7910  seqomlem3  8397  1on  8423  2on  8425  inf0  9556  scottexs  9822  kardex  9829  infxpenlem  9948  r1om  10179  cfon  10190  fin23lem16  10270  fin1a2lem6  10340  hsmexlem5  10365  brdom7disj  10466  brdom6disj  10467  1lt2pi  10840  0cn  11146  resubcli  11462  0reALT  11497  1nn  12163  10nn  12633  numsucc  12657  nummac  12662  unirnioo  13365  ioorebas  13367  fz0to4untppr  13543  om2uzrani  13856  uzrdg0i  13863  hashunlei  14324  cats1fvn  14746  trclubi  14880  4sqlem19  16834  dec2dvds  16934  mod2xnegi  16942  modsubi  16943  gcdi  16944  isstruct2  17020  grppropstr  18766  nn0srg  20865  ltbval  21442  sn0topon  22346  indistop  22350  indisuni  22351  indistps2  22360  indistps2ALT  22363  restbas  22507  leordtval2  22561  iocpnfordt  22564  icomnfordt  22565  iooordt  22566  reordt  22567  dis1stc  22848  ptcmpfi  23162  ustfn  23551  ustn0  23570  retopbas  24122  blssioo  24156  xrtgioo  24167  zcld  24174  cnperf  24181  retopconn  24190  iimulcn  24299  rembl  24902  mbfdm  24988  ismbf  24990  mbf0  24996  bddiblnc  25204  abelthlem9  25797  advlog  26007  advlogexp  26008  2irrexpq  26083  cxpcn3  26099  loglesqrt  26109  log2ub  26297  ppi1i  26515  cht2  26519  cht3  26520  bpos1lem  26628  lgslem4  26646  vmadivsum  26828  log2sumbnd  26890  selberg2  26897  selbergr  26914  nogt01o  27042  iscgrg  27452  ishpg  27699  ax5seglem7  27882  h2hva  29914  h2hsm  29915  h2hnm  29916  norm-ii-i  30077  hhshsslem2  30208  shincli  30302  chincli  30400  lnophdi  30942  imaelshi  30998  rnelshi  30999  bdophdi  31037  dfdec100  31721  dpadd2  31761  dpmul  31764  dpmul4  31765  nn0omnd  32132  nn0archi  32134  fermltlchr  32149  znfermltl  32150  ccfldextrr  32328  lmatfvlem  32387  rmulccn  32500  rrhre  32593  sigaex  32700  br2base  32860  sxbrsigalem3  32863  carsgclctunlem3  32911  sitmcl  32942  rpsqrtcn  33197  hgt750lem  33255  hgt750lem2  33256  afsval  33275  kur14lem7  33797  retopsconn  33834  satfvsuclem1  33944  fmlasuc0  33969  hfuni  34760  neibastop2lem  34823  onint1  34912  bj-snfromadj  35506  topdifinffinlem  35809  poimirlem9  36078  poimirlem28  36097  poimirlem30  36099  poimirlem32  36101  ftc1cnnc  36141  cncfres  36215  lineset  38192  lautset  38536  pautsetN  38552  tendoset  39213  decpmulnc  40779  decpmul  40780  areaquad  41528  0no  41689  finonex  41708  sblpnf  42572  lhe4.4ex1a  42591  fourierdlem62  44381  fourierdlem76  44395  65537prm  45740  11gbo  45939  bgoldbtbndlem1  45969  seppcld  46934
  Copyright terms: Public domain W3C validator