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

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

Proof of Theorem eqeltri
StepHypRef Expression
1 eqeltri.2 . 2 𝐵𝐶
2 eqeltri.1 . . 3 𝐴 = 𝐵
32eleq1i 2883 . 2 (𝐴𝐶𝐵𝐶)
41, 3mpbir 234 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  wcel 2112
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2794  df-clel 2873
This theorem is referenced by:  eqeltrri  2890  3eltr4i  2906  intab  4871  unisn2  5183  inex2  5189  vpwex  5246  ord3ex  5256  zfpair  5290  opex  5324  otex  5325  uniopel  5374  elvvuni  5596  predasetex  6135  isarep2  6417  fvex  6662  fvexi  6663  riotaex  7101  ovexi  7173  tpex  7454  oprabex  7663  oprabrexex2  7665  mpoexw  7763  tfrlem16  8016  1on  8096  2on  8098  2oex  8099  3on  8101  4on  8102  oesuclem  8137  oecl  8149  o2p2e4  8153  nnecl  8226  1onn  8252  2onn  8253  3onn  8254  4onn  8255  mapsnf1o2  8445  sbthlem10  8624  nnunifi  8757  xpfi  8777  prfi  8781  tpfi  8782  fnfi  8784  pwfi  8807  fczfsuppd  8839  cantnfvalf  9116  oemapwe  9145  cantnffval2  9146  cnfcom3clem  9156  r1fin  9190  hta  9314  infxpenlem  9428  alephon  9484  alephfplem1  9519  dfac5lem4  9541  dfac5lem5  9542  kmlem10  9574  fin1a2lem10  9824  fin1a2lem12  9826  hsmexlem9  9840  axcc2lem  9851  domtriomlem  9857  axdc2lem  9863  axcclem  9872  brdom7disj  9946  brdom6disj  9947  iundom2g  9955  konigthlem  9983  canthwelem  10065  wunex2  10153  wunex3  10156  1nq  10343  1pr  10430  nrex1  10479  axcnex  10562  ax1cn  10564  pnfex  10687  mnfxr  10691  inelr  11619  cju  11625  nnexALT  11631  2nn  11702  2re  11703  2cn  11704  3nn  11708  3re  11709  3cn  11710  4nn  11712  4re  11713  4cn  11714  5nn  11715  5re  11716  5cn  11717  6nn  11718  6re  11719  6cn  11720  7nn  11721  7re  11722  7cn  11723  8nn  11724  8re  11725  8cn  11726  9nn  11727  9re  11728  9cn  11729  nn0ex  11895  zexALT  11993  nneo  12058  zeo  12060  deccl  12105  10re  12109  decnncl  12110  numnncl2  12113  decnncl2  12114  numsucc  12130  numma2c  12136  numadd  12137  numaddc  12138  nummul1c  12139  nummul2c  12140  decmul1  12154  qexALT  12355  xrex  12378  xnegex  12593  xnegcl  12598  ixxssxr  12742  om2uzuzi  13316  ltweuz  13328  axdc4uzlem  13350  seqex  13370  seqexw  13384  m1expcl2  13451  faccl  13643  facwordi  13649  faclbnd2  13651  bccl  13682  hashen1  13731  hashrabrsn  13733  hashunlei  13786  hashpw  13797  s1cli  13954  ccat2s1p1  13980  cats1un  14078  revs1  14122  cshwsexa  14181  cats1cli  14214  cats1fvn  14215  crre  14469  remim  14472  climmpt  14924  sumex  15040  supcvg  15207  geo2lim  15227  prodex  15257  bpoly4  15409  ere  15438  eftlub  15458  efsep  15459  tan0  15500  ef01bndlem  15533  nn0o  15728  divalglem5  15742  divalglem9  15746  sadcf  15796  smupf  15821  crth  16109  phimullem  16110  pczpre  16178  pockthi  16237  prmreclem2  16247  igz  16264  0ramcl  16353  1259lem1  16460  1259lem2  16461  1259lem3  16462  1259lem4  16463  1259lem5  16464  1259prm  16465  2503lem1  16466  2503lem2  16467  2503lem3  16468  2503prm  16469  4001lem1  16470  4001lem2  16471  4001lem3  16472  4001lem4  16473  4001prm  16474  ndxarg  16504  basendxnn  16544  strle1  16588  prdsbasex  16720  prdsds  16733  yonedalem3  17526  isposix  17563  plusffval  17854  efmnd1hash  18053  efmnd2hash  18055  smndex1bas  18067  smndex1sgrp  18069  smndex1mnd  18071  smndex1id  18072  smndex2dbas  18075  smndex2hbas  18077  grpsubfval  18143  mulgfval  18222  symg1hash  18514  symg2hash  18516  symgvalstruct  18521  symgfisg  18592  psgnsn  18644  psgnprfval1  18646  odfval  18656  sylow2alem2  18739  efgsval2  18855  efgsp1  18859  pgpfaclem1  19200  dvdsrval  19395  isirred  19449  scaffval  19649  xrsex  20110  zlmlem  20214  znle  20232  znidomb  20257  cnmsgnsubg  20270  refld  20312  ipffval  20341  psrbag0  20737  psrbagsn  20738  psr1baslem  20818  mat1dimbas  21081  mat1dimscm  21084  mat1f1o  21087  mat1rhmelval  21089  m2detleib  21240  pmatcoe1fsupp  21310  indistopon  21610  iccordt  21823  conncompid  22040  ptbasfi  22190  ptcmpfi  22422  ustfn  22811  ust0  22829  ustn0  22830  tmslem  23093  nmfval  23199  tnglem  23250  cnbl0  23383  cnopn  23396  remet  23399  re2ndc  23410  zcld  23422  icccmp  23434  xrge0gsumle  23442  xrge0tsms  23443  xmetdcn  23447  divcn  23477  expcn  23481  iiconn  23496  idcncf  23527  cnmpopc  23537  cnrehmeo  23562  cnheiborlem  23563  rellycmp  23566  bndth  23567  evth2  23569  cnrlmod  23752  cnrlvec  23753  cncmet  23930  ishl2  23978  ehleudis  24026  ehleudisval  24027  finiunmbl  24152  ioombl1lem4  24169  vitalilem4  24219  vitalilem5  24220  ismbf2d  24248  mbfimaopnlem  24263  mbfi1fseqlem6  24328  itgex  24378  bddmulibl  24446  ditgex  24459  recnperf  24512  dvcnvrelem2  24625  ftc1  24649  mdegcl  24674  plyeq0lem  24811  aaliou3lem4  24946  dvradcnv  25020  sincn  25043  coscn  25044  tanabsge  25103  circsubm  25149  reloggim  25194  logcn  25242  dvloglem  25243  logdmopn  25244  dvlog2  25248  2irrexpq  25325  cxpcn  25338  cxpcn3  25341  resqrtcn  25342  2logb9irrALT  25388  2irrexpqALT  25390  atanrecl  25501  atan1  25518  atansopn  25522  birthdaylem1  25541  birthday  25544  emcllem4  25588  emcllem6  25590  lgamgulmlem6  25623  basellem6  25675  ppiublem1  25790  bposlem6  25877  bposlem8  25879  lgslem4  25888  lgsdir2lem2  25914  selberglem1  26133  selberglem3  26135  selberg  26136  selbergs  26162  qdrng  26208  edgfndxnn  26789  structvtxvallem  26817  usgrexmpllem  27054  usgrexmpl  27057  uhgrspan1  27097  upgrres  27100  umgrres  27101  usgrres  27102  upgrres1  27107  umgrres1  27108  usgrres1  27109  fusgrfis  27124  cusgrres  27242  vtxdlfgrval  27279  vtxdusgr0edgnelALT  27290  umgr2v2e  27319  vtxdginducedm1lem1  27333  vtxdginducedm1fi  27338  finsumvtxdg2ssteplem4  27342  pthdlem1  27559  crctcshlem3  27609  2wlkd  27726  2wlkond  27727  2trlond  27729  2pthd  27730  2pthond  27732  umgr2adedgwlkonALT  27737  0pth  27914  wlk2v2e  27946  3wlkd  27959  3trlond  27962  3pthd  27963  3pthond  27964  3spthond  27966  eupthvdres  28024  eulerpathpr  28029  konigsbergumgr  28040  konigsberglem5  28045  konigsberg  28046  ex-lcm  28247  isvciOLD  28367  isnvi  28400  blocni  28592  hmoval  28597  cncph  28606  ipasslem7  28623  siilem2  28639  normlem2  28898  normlem3  28899  normlem6  28902  h0elch  29042  hhssabloilem  29048  hhsssh  29056  spansnji  29433  nonbooli  29438  3oalem5  29453  3oalem6  29454  3oai  29455  mayetes3i  29516  nmcexi  29813  nmbdfnlb  29837  rnelshi  29846  cnlnadjlem5  29858  pjbdlni  29936  golem2  30059  goeqi  30060  dp2clq  30587  rpdp2cl  30588  rpdp2cl2  30589  dpmul100  30603  rpdpcl  30609  xrge0tsmsd  30746  pmtrto1cl  30795  psgnfzto1stlem  30796  fzto1st  30799  psgnfzto1st  30801  nn0omnd  30969  xrge0slmod  30972  fply1  30986  prmidl0  31038  ccfldextdgrr  31149  circtopn  31194  circcn  31195  zarcmplem  31238  tpr2tp  31261  tpr2rico  31269  ordtprsval  31275  ordtprsuni  31276  ordtrestNEW  31278  ordtrest2NEWlem  31279  ordtrest2NEW  31280  ordtconnlem1  31281  mndpluscn  31283  xrge0pluscn  31297  xrge0mulc1cn  31298  xrge0haus  31301  lmlimxrge0  31305  lmxrge0  31309  qqhcn  31346  qqhucn  31347  esumex  31402  esumcst  31436  hasheuni  31458  esumcvg  31459  prsiga  31504  brsiga  31556  mbfmcnt  31640  sxbrsigalem3  31644  dya2iocuni  31655  dya2iocucvr  31656  sxbrsigalem1  31657  sxbrsiga  31662  eulerpartlemt  31743  fibp1  31773  coinflipprob  31851  coinfliprv  31854  ccatmulgnn0dir  31926  signswplusg  31939  hgt750lem2  32037  hgt750leme  32043  bnj105  32108  bnj918  32151  bnj95  32250  bnj852  32307  bnj865  32309  subfacp1lem1  32540  subfacp1lem3  32543  subfacp1lem5  32545  subfacp1lem6  32546  kur14lem7  32573  iisconn  32613  iillysconn  32614  cvmliftlem5  32650  cvmliftlem8  32653  cvmliftlem10  32655  cvmlift2lem9  32672  satfv0  32719  goalrlem  32757  goalr  32758  satffunlem2lem2  32767  circum  33031  iexpire  33081  trpredex  33190  altopex  33535  colinearex  33635  ssoninhaus  33910  cnndvlem2  33991  bj-pinftyccb  34637  taupi  34738  isbasisrelowl  34776  relowlpssretop  34782  poimirlem29  35085  poimirlem30  35086  poimirlem31  35087  dvasin  35140  dvacos  35141  areacirc  35149  upixp  35166  fdc  35182  lmclim2  35195  cncfres  35202  heibor1lem  35246  rrnval  35264  rrnmet  35266  reheibor  35276  isdrngo2  35395  isrngohom  35402  idlval  35450  isidl  35451  igenval  35498  scottexf  35605  cnvepresex  35750  renegclALT  36258  ldualfvadd  36423  cmtfvalN  36505  cvrfval  36563  cdleme31fv  37685  cdlemk40  38212  cdlemk56  38266  dibopelvalN  38438  dibopelval2  38440  dibelval3  38442  diblsmopel  38466  cdlemn11a  38502  dihopelvalcpre  38543  dihpN  38631  hlhilsca  39230  hlhilip  39243  3factsumint1  39308  lcmineqlem23  39338  3lexlogpow5ineq1  39340  sn-0tie0  39569  itrere  39584  retire  39585  prjspval  39590  mapfzcons2  39653  jm2.23  39930  jm2.27dlem2  39944  jm2.27dlem4  39946  rmydioph  39948  rmxdioph  39950  expdiophlem2  39956  expdioph  39957  aomclem6  39996  pwslnmlem0  40028  frlmpwfi  40035  mncn0  40076  aaitgo  40099  arearect  40158  areaquad  40159  comptiunov2i  40400  frege110  40667  frege133  40690  scottex2  40946  radcnvrat  41011  uzmptshftfval  41043  dvradcnv2  41044  binomcxplemdvbinom  41050  binomcxplemcvg  41051  binomcxplemnotnn0  41053  rfcnpre1  41641  fcnre  41647  refsumcn  41652  refsum2cnlem1  41659  unirnmapsn  41836  infxrpnf  42077  iocopn  42150  icoopn  42155  mccl  42233  clim1fr1  42236  islptre  42254  sumnnodd  42265  lptre2pt  42275  limclner  42286  limclr  42290  expfac  42292  0cnf  42512  icccncfext  42522  ioodvbdlimc1lem2  42567  ioodvbdlimc2lem  42569  itgsin0pilem1  42585  iblempty  42600  itgvol0  42603  stoweidlem47  42682  stoweidlem53  42688  stoweidlem57  42692  stoweidlem59  42694  wallispilem3  42702  wallispilem4  42703  wallispilem5  42704  wallispi  42705  stirlinglem1  42709  stirlinglem8  42716  stirlinglem12  42720  stirlinglem13  42721  stirlinglem14  42722  stirlinglem15  42723  dirkerper  42731  dirkercncflem2  42739  fourierdlem16  42758  fourierdlem21  42763  fourierdlem22  42764  fourierdlem36  42778  fourierdlem42  42784  fourierdlem71  42812  fourierdlem83  42824  fourierdlem102  42843  fourierdlem103  42844  fourierdlem104  42845  fourierdlem111  42852  fourierdlem112  42853  fourierdlem114  42855  sqwvfoura  42863  sqwvfourb  42864  fourierswlem  42865  fouriersw  42866  etransclem48  42917  salexct3  42975  salgencntex  42976  salgensscntex  42977  iooborel  42984  bor1sal  42988  gsumge0cl  43003  sge0tsms  43012  sge0isum  43059  nnfoctbdjlem  43087  isomenndlem  43162  mbfresmf  43366  incsmflem  43368  incsmf  43369  smfmbfcex  43386  decsmflem  43392  decsmf  43393  smflimlem1  43397  smfpimbor1lem2  43424  smf2id  43426  smfco  43427  smfpimcclem  43431  sprsymrelfolem1  44002  sprbisymrel  44009  fmtno0prm  44068  fmtno1prm  44069  fmtno2prm  44070  fmtno3prm  44072  fmtno4prm  44085  m2prm  44101  m3prm  44102  m5prm  44108  m7prm  44110  lighneallem4a  44119  0evenALTV  44199  1oddALTV  44201  2evenALTV  44203  6even  44222  7odd  44223  8even  44224  9gbo  44285  strisomgrop  44351  ushrisomgr  44352  uspgrex  44371  issubmgm2  44403  lmod1zrnlvec  44896  zlmodzxzldeplem1  44902  zlmodzxzldeplem3  44904  zlmodzxzldeplem4  44905  zlmodzxzldep  44906  ldepsnlinclem1  44907  ldepsnlinclem2  44908  blennn0elnn  44984  nn0sumshdiglemA  45026  nn0sumshdiglemB  45027  itcovalpclem2  45078  itcovalt2lem2  45083  ackval42  45103  rrx2line  45147  rrx2linesl  45150  spheres  45153  2sphere  45156  2sphere0  45157  line2x  45161  line2y  45162
  Copyright terms: Public domain W3C validator