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

Theorem eqeltrri 2856
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 2787 . 2 𝐵 = 𝐴
3 eqeltrri.2 . 2 𝐴𝐶
42, 3eqeltri 2855 1 𝐵𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1601  wcel 2107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-ext 2754
This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-cleq 2770  df-clel 2774
This theorem is referenced by:  3eltr3i  2871  zfrep4  5017  p0ex  5097  pp0ex  5099  ord3ex  5100  zfpair  5138  epse  5340  unex  7235  fvresex  7420  opabex3  7426  abexssex  7429  abexex  7430  oprabrexex2  7437  seqomlem3  7832  inf0  8817  scottexs  9049  kardex  9056  infxpenlem  9171  r1om  9403  cfon  9414  fin23lem16  9494  fin1a2lem6  9564  hsmexlem5  9589  brdom7disj  9690  brdom6disj  9691  1lt2pi  10064  0cn  10370  resubcli  10687  0reALT  10722  1nn  11391  10nn  11865  numsucc  11890  nummac  11895  unirnioo  12590  ioorebas  12592  fz0to4untppr  12765  om2uzrani  13074  uzrdg0i  13081  hashunlei  13530  cats1fvn  14013  trclubi  14148  4sqlem19  16075  dec2dvds  16175  mod2xnegi  16183  modsubi  16184  gcdi  16185  isstruct2  16269  grppropstr  17830  ltbval  19872  nn0srg  20216  sn0topon  21214  indistop  21218  indisuni  21219  indistps2  21228  indistps2ALT  21230  restbas  21374  leordtval2  21428  iocpnfordt  21431  icomnfordt  21432  iooordt  21433  reordt  21434  dis1stc  21715  ptcmpfi  22029  ustfn  22417  ustn0  22436  retopbas  22976  blssioo  23010  xrtgioo  23021  zcld  23028  cnperf  23035  retopconn  23044  iimulcn  23149  rembl  23748  mbfdm  23834  ismbf  23836  mbf0  23842  abelthlem9  24635  advlog  24841  advlogexp  24842  2irrexpq  24917  cxpcn3  24933  loglesqrt  24943  log2ub  25132  ppi1i  25350  cht2  25354  cht3  25355  bpos1lem  25463  lgslem4  25481  vmadivsum  25627  log2sumbnd  25689  selberg2  25696  selbergr  25713  iscgrg  25867  ishpg  26111  ax5seglem7  26288  fusgrfis  26681  h2hva  28407  h2hsm  28408  h2hnm  28409  norm-ii-i  28570  hhshsslem2  28701  shincli  28797  chincli  28895  lnophdi  29437  imaelshi  29493  rnelshi  29494  bdophdi  29532  dfdec100  30144  dpadd2  30184  dpmul  30187  dpmul4  30188  nn0omnd  30407  nn0archi  30409  lmatfvlem  30483  rmulccn  30576  rrhre  30667  sigaex  30774  br2base  30933  sxbrsigalem3  30936  carsgclctunlem3  30984  sitmcl  31015  rpsqrtcn  31277  hgt750lem  31335  hgt750lem2  31336  afsval  31355  kur14lem7  31797  retopsconn  31834  hfuni  32884  neibastop2lem  32947  onint1  33035  topdifinffinlem  33793  cnfin0  33838  cnfinltrel  33839  poimirlem9  34049  poimirlem28  34068  poimirlem30  34070  poimirlem32  34072  bddiblnc  34110  ftc1cnnc  34114  cncfres  34193  lineset  35897  lautset  36241  pautsetN  36257  tendoset  36918  decpmulnc  38159  decpmul  38160  areaquad  38770  sblpnf  39475  lhe4.4ex1a  39494  fourierdlem62  41322  fourierdlem76  41336  65537prm  42519  11gbo  42698  bgoldbtbndlem1  42728
  Copyright terms: Public domain W3C validator