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

Theorem eleq2 2689
Description: Equality implies equivalence of membership. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 20-Nov-2019.)
Assertion
Ref Expression
eleq2 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))

Proof of Theorem eleq2
StepHypRef Expression
1 id 22 . 2 (𝐴 = 𝐵𝐴 = 𝐵)
21eleq2d 2686 1 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1482  wcel 1989
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1704  df-cleq 2614  df-clel 2617
This theorem is referenced by:  eleq12  2690  eleq2i  2692  nelneq2  2725  dvelimdc  2785  nelne1  2889  raleqf  3132  rexeqf  3133  reueq1f  3134  rmoeq1f  3135  raleleq  3154  rabeqf  3188  clel3g  3338  clel4  3340  sbcbi2  3482  sbcel2gv  3494  csbeq2  3535  difeq2  3720  uneq1  3758  ineq1  3805  unineq  3875  n0i  3918  sbnfc2  4005  disjel  4021  elif  4126  exsnrex  4219  elinsn  4243  sneqrg  4368  preq1b  4375  preqr1OLD  4378  preq12b  4380  prel12  4381  elpreqprb  4395  elunii  4439  eluniab  4445  ssuniOLD  4458  elinti  4483  elintab  4485  intss1  4490  intmin  4495  intab  4505  iineq2  4536  dfiin2g  4551  breq  4653  zfrepclf  4775  zfauscl  4781  sseliALT  4789  inuni  4824  elALT  4908  rext  4914  intid  4924  elopg  4932  opth1  4942  opthwiener  4974  xpeq1  5126  xpeq2  5127  0nelelxp  5143  opthprc  5165  ordtri1  5754  ordtri3  5757  ordtri3OLD  5758  nsuceq0  5803  suctr  5806  suctrOLD  5807  ordnbtwn  5814  ordnbtwnOLD  5815  funopg  5920  dffv2  6269  fveqdmss  6352  dffo4  6373  funopdmsn  6412  fnsnb  6429  elunirn  6506  f1oiso  6598  canth  6605  eusvobj2  6640  mpt2eq123  6711  ndmovg  6814  snnexOLD  6964  uniuni  6968  iunpw  6975  oneqmin  7002  onuninsuci  7037  nlimsucg  7039  limomss  7067  nnlim  7075  peano5  7086  unielxp  7201  cnvf1o  7273  smoel  7454  smo11  7458  tz7.44-2  7500  oawordeulem  7631  oaordex  7635  omordi  7643  oneo  7658  oeordi  7664  oeoa  7674  oeoe  7676  nnmordi  7708  nnaordex  7715  omabs  7724  nnneo  7728  omsmolem  7730  elqsn0  7813  qsel  7823  mapsn  7896  undifixp  7941  boxriin  7947  boxcutc  7948  fineqvlem  8171  fineqv  8172  pssnn  8175  fissuni  8268  dffi2  8326  inficl  8328  dffi3  8334  wofib  8447  zfregcl  8496  zfregclOLD  8498  en3lplem1  8508  en3lp  8510  suc11reg  8513  inf0  8515  inf3lem2  8523  inf3lem3  8524  infeq5i  8530  axinf2  8534  dfom3  8541  elom3  8542  cantnfle  8565  oemapvali  8578  cantnflem1c  8581  cantnflem1  8583  tc2  8615  r1sdom  8634  rankwflemb  8653  rankval3b  8686  rankunb  8710  rankuni2b  8713  tcrank  8744  cardlim  8795  cardprclem  8802  infxpenlem  8833  alephnbtwn  8891  alephordi  8894  cardaleph  8909  alephfp  8928  alephval3  8930  dfac3  8941  dfac5lem2  8944  dfac5lem4  8946  dfac2  8950  kmlem2  8970  coflim  9080  cfsmolem  9089  fin23lem30  9161  isf32lem2  9173  isf34lem4  9196  axdc2lem  9267  axdc3lem2  9270  axdc3lem4  9272  axdc4lem  9274  zorn2lem7  9321  axdclem  9338  brdom7disj  9350  brdom6disj  9351  axpowndlem3  9418  winainflem  9512  iswun  9523  eltskg  9569  inar1  9594  elgrug  9611  inaprc  9655  eltskm  9662  addnidpi  9720  indpi  9726  nqereu  9748  elnp  9806  elnpi  9807  genpnnp  9824  ltaddpr  9853  dfnn2  11030  dfnn3  11031  dfuzi  11465  uz11  11707  elfzonlteqm1  12539  om2uzlti  12744  axdc4uz  12778  hashrabsn1  13158  hashbclem  13231  hashf1lem2  13235  hash2prb  13249  hash2prd  13252  wrdsymb0  13334  lsw0  13347  rtrclreclem3  13794  prodeq1f  14632  rpnnen2lem1  14937  rpnnen2lem2  14938  sadcp1  15171  lcmfval  15328  lcmf0val  15329  ismre  16244  isacs  16306  initoid  16649  termoid  16650  initoeu2lem1  16658  clatl  17110  mreclatBAD  17181  issubm  17341  dfgrp2e  17442  cycsubg  17616  isnsg  17617  subgacs  17623  nsgacs  17624  resghm  17670  ghmeql  17677  gsmsymgreq  17846  f1otrspeq  17861  pmtrval  17865  pmtrdifellem4  17893  pmtrprfval  17901  gsumzsplit  18321  pgpfac1lem1  18467  pgpfac1lem5  18472  pgpfac1  18473  issubrg  18774  lmodfopnelem2  18894  islss  18929  lssacs  18961  lspsneq0  19006  lmhmeql  19049  lspdisjb  19120  lidl1el  19212  lidldvgen  19249  0ring01eq  19265  mplcoe1  19459  mplcoe5  19462  islindf4  20171  m1detdiag  20397  mdetunilem9  20420  maducoeval2  20440  madugsum  20443  chpmat1dlem  20634  istopg  20694  toprntopon  20723  fiinbas  20750  topbas  20770  ppttop  20805  pptbas  20806  epttop  20807  elcls  20871  clsndisj  20873  elcls3  20881  iscldtop  20893  neiptopnei  20930  restbas  20956  restntr  20980  pnfnei  21018  mnfnei  21019  cnpimaex  21054  lmcvg  21060  iscnp4  21061  cncnpi  21076  cnconst2  21081  cnprest  21087  cnprest2  21088  cnpdis  21091  lmss  21096  lmff  21099  cnt0  21144  ist1-3  21147  cnhaus  21152  isreg2  21175  dishaus  21180  ordthauslem  21181  cmpsublem  21196  cmpsub  21197  cmpcld  21199  hauscmplem  21203  unconn  21226  conncompid  21228  conncompconn  21229  conncompss  21230  1stcfb  21242  1stcrest  21250  2ndcctbss  21252  2ndcomap  21255  dis2ndc  21257  1stcelcls  21258  llyeq  21267  nllyeq  21268  restnlly  21279  islly2  21281  lly1stc  21293  dislly  21294  hauspwdom  21298  finlocfin  21317  unisngl  21324  dissnlocfin  21326  locfindis  21327  comppfsc  21329  llycmpkgen2  21347  txbas  21364  eltx  21365  ptpjopn  21409  ptclsg  21412  dfac14lem  21414  txcnp  21417  ptcnplem  21418  ptcnp  21419  txlly  21433  pthaus  21435  txtube  21437  txhaus  21444  txlm  21445  tx1stc  21447  txkgen  21449  xkohaus  21450  xkopt  21452  xkococnlem  21456  tgqtop  21509  kqfvima  21527  kqt0lem  21533  isr0  21534  r0cld  21535  regr1lem  21536  kqreglem1  21538  kqreglem2  21539  reghmph  21590  fbssfi  21635  isfil  21645  filuni  21683  isufil  21701  isufil2  21706  uffix  21719  fixufil  21720  uffixfr  21721  uffixsn  21723  rnelfm  21751  flimopn  21773  flimrest  21781  flimcls  21783  flftg  21794  txflf  21804  fclsopni  21813  fclsrest  21822  fclscf  21823  fcfnei  21833  alexsublem  21842  alexsubALTlem3  21847  alexsubALT  21849  tmdgsum2  21894  symgtgp  21899  subgntr  21904  opnsubg  21905  tgpconncompeqg  21909  ghmcnp  21912  tgpt0  21916  qustgpopn  21917  tsmsi  21931  tsmssubm  21940  tsmssplit  21949  isust  22001  ustn0  22018  blssps  22223  blss  22224  blssexps  22225  blssex  22226  neibl  22300  blcld  22304  metss  22307  methaus  22319  met1stc  22320  met2ndci  22321  metrest  22323  prdsxmslem2  22328  metcnp3  22339  dscopn  22372  idnghm  22541  qdensere  22567  tgioo  22593  tgqioo  22597  zdis  22613  xrge0tsms  22631  cnheibor  22748  lmmbr  23050  bcthlem4  23118  ovolicc2lem5  23283  dyadmbllem  23361  i1fd  23442  itg11  23452  itg2gt0  23521  itgeq1f  23532  bddmulibl  23599  ellimc2  23635  limcnlp  23636  ellimc3  23637  limcflf  23639  limciun  23652  lhop1lem  23770  ig1pdvds  23930  plycpn  24038  aannenlem2  24078  efopn  24398  xrlimcnp  24689  wilthlem2  24789  wilthlem3  24790  wilth  24791  tghilberti1  25526  tghilberti2  25527  colline  25538  lmif  25671  islmib  25673  incistruhgr  25968  upgr1eopALT  26006  uhgrvtxedgiedgb  26025  upgredg2vtx  26030  edglnl  26032  numedglnl  26033  uhgr2edg  26094  umgrvad2edg  26099  umgr2edgneu  26100  usgredg4  26103  usgredg2vtxeuALT  26108  uspgredg2vlem  26109  uspgredg2v  26110  ushgredgedg  26115  nbgr1vtx  26248  nbusgredgeu0  26264  nbusgrf1o0  26265  nbusgrf1o  26267  nb3grprlem1  26276  nb3grprlem2  26277  uvtxa01vtx0  26291  nbupgruvtxres  26302  cplgr1vlem  26319  cplgr1v  26320  vtxd0nedgb  26378  vtxduhgr0nedg  26382  1loopgrvd2  26393  1egrvtxdg0  26401  uspgrloopvtxel  26406  vtxdginducedm1lem4  26432  wlk1walk  26529  wlkp1lem1  26564  pthdivtx  26619  0enwwlksnge1  26743  umgrwwlks2on  26844  rusgr0edg  26862  eleclclwwlksn  26946  upgr4cycl4dv4e  27038  1conngr  27047  vdn0conngrumgrv2  27049  eupth2eucrct  27070  eupth2lem1  27071  frgrncvvdeqlem7  27162  frgrncvvdeqlem9  27164  frgrwopreg1  27173  frgrwopreg2  27174  l2p  27315  lpni  27316  issh  28049  pjoc1  28277  h1dn0  28395  spansneleqi  28412  nonbooli  28494  pjch  28537  pjnel  28569  cdjreui  29275  rexunirn  29315  rabsnel  29325  opabdm  29407  opabrn  29408  fpwrelmapffslem  29492  fpwrelmap  29493  fz1nntr  29546  xrge0tsmsd  29770  reff  29891  tpr2rico  29943  lmxrge0  29983  indval  30060  issiga  30159  isrnsigaOLD  30160  isrnsiga  30161  isldsys  30204  isros  30216  issros  30223  ddeval1  30282  ddeval0  30283  ddemeas  30284  ismbfm  30299  isanmbfm  30303  dya2icoseg  30324  dya2iocnrect  30328  ballotlem7  30582  bnj145OLD  30780  bnj216  30785  bnj563  30798  bnj956  30832  bnj545  30950  bnj548  30952  bnj570  30960  bnj900  30984  bnj929  30991  bnj964  30998  bnj983  31006  bnj1001  31013  bnj1145  31046  bnj1398  31087  bnj1498  31114  erdszelem1  31158  kur14lem9  31181  cnllysconn  31212  cvmcov  31230  cvmsss2  31241  cvmcov2  31242  cvmseu  31243  cvmsiota  31244  cvmopnlem  31245  cvmliftlem15  31265  mclsssvlem  31444  mclsind  31452  untelirr  31570  untsucf  31572  elintfv  31648  dfon2lem4  31675  dfon2lem7  31678  dfon2lem9  31680  soseq  31735  frrlem4  31767  frrlem5e  31772  frrlem11  31776  nodenselem8  31825  noetalem3  31849  nocvxminlem  31877  dfiota3  32014  funpartlem  32033  funpartfun  32034  linethru  32244  hilbert1.1  32245  hilbert1.2  32246  rankelg  32259  elhf2  32266  fneint  32327  neibastop2lem  32339  bj-rabeqd  32900  bj-cleq  32933  bj-snsetex  32935  bj-nuliota  33003  mptsnunlem  33165  isbasisrelowllem1  33183  isbasisrelowllem2  33184  relowlssretop  33191  relowlpssretop  33192  finxpeq1  33203  finxpreclem5  33212  finxpreclem6  33213  unccur  33372  fin2so  33376  matunitlindflem1  33385  ptrecube  33389  poimirlem9  33398  poimirlem30  33419  poimir  33422  heicant  33424  mblfinlem1  33426  ftc1anc  33473  ftc2nc  33474  cover2  33488  isbnd2  33562  prdstotbnd  33573  heibor1lem  33588  grpokerinj  33672  rngoueqz  33719  isidl  33793  1idl  33805  0rngo  33806  ispridl  33813  smprngopr  33831  isfldidl  33847  isdmn3  33853  mpt2bi123f  33951  iineq12f  33953  mptbi12f  33955  lsateln0  34108  ispsubsp  34857  linepsubN  34864  elpcliN  35005  dvh3dim3N  36564  dochsnnz  36565  mapdindp3  36837  elmzpcl  37115  diophren  37203  dford3lem2  37420  ttac  37429  pw2f1ocnv  37430  wepwsolem  37438  kelac1  37459  sdrgacs  37597  elintabg  37706  elmapintrab  37708  intabssd  37742  eliunov2  37797  gneispaceel2  38268  expgrowthi  38358  dvconstbi  38359  tratrb  38572  suctrALT2VD  38897  suctrALT2  38898  en3lplem1VD  38904  en3lpVD  38906  tratrbVD  38923  suctrALTcf  38984  suctrALTcfVD  38985  suctrALT3  38986  unisnALT  38988  elunif  39001  fnchoice  39014  restuni3  39127  mapsnd  39210  supminfxr  39513  icccncfext  39869  stoweidlem27  40013  stoweidlem35  40021  stoweidlem46  40032  stoweidlem52  40038  ioorrnopnlem  40293  ioorrnopnxrlem  40295  issal  40303  intsaluni  40316  salgencntex  40330  sge0f1o  40368  smfresal  40764  funressnfv  40977  fnbrafvb  41003  afvco2  41025  ndmaovg  41033  aovmpt4g  41050  fzoopth  41106  nnsum4primeseven  41459  nnsum4primesevenALTV  41460  sprsymrelf1lem  41512  issubmgm  41560  c0snmgmhm  41685  c0snmhm  41686  rngccatidALTV  41760  ringccatidALTV  41823  ldepspr  42033
  Copyright terms: Public domain W3C validator