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

Theorem eleq2 2540
Description: Equality implies equivalence of membership. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 20-Nov-2019.)
Assertion
Ref Expression
eleq2  |-  ( A  =  B  ->  ( C  e.  A  <->  C  e.  B ) )

Proof of Theorem eleq2
StepHypRef Expression
1 id 22 . 2  |-  ( A  =  B  ->  A  =  B )
21eleq2d 2537 1  |-  ( A  =  B  ->  ( C  e.  A  <->  C  e.  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1379    e. wcel 1767
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-cleq 2459  df-clel 2462
This theorem is referenced by:  eleq12  2543  eleq2i  2545  eleq2dOLD  2548  nelneq2  2585  dvelimdc  2652  nelne1  2796  neleq2OLD  2808  raleqf  3054  rexeqf  3055  reueq1f  3056  rmoeq1f  3057  rabeqf  3106  clel3g  3241  clel4  3243  sbcbi2  3382  sbcel2gv  3398  csbeq2  3439  difeq2  3616  uneq1  3651  ineq1  3693  unineq  3748  n0i  3790  sbnfc2  3854  disjel  3873  elif  3979  exsnrex  4065  sneqr  4194  preqr1  4200  preq12b  4202  prel12  4203  elunii  4250  eluniab  4256  ssuni  4267  elinti  4291  elintab  4293  intss1  4297  intmin  4302  intab  4312  iineq2  4343  dfiin2g  4358  breq  4449  zfrepclf  4564  axsep2  4569  zfauscl  4570  sseliALT  4578  inuni  4609  pwne0  4617  elALT  4690  rext  4695  intid  4705  opth1  4720  opthwiener  4749  ordtri1  4911  ordtri3  4914  nsuceq0  4958  suctr  4961  ordnbtwn  4968  xpeq1  5013  xpeq2  5014  opthprc  5047  funopg  5620  dffv2  5940  dffo4  6037  fnsnb  6080  elunirn  6151  f1oiso  6235  canth  6242  eusvobj2  6277  mpt2eq123  6340  ndmovg  6442  snnex  6590  uniuni  6593  iunpw  6598  oneqmin  6624  onuninsuci  6659  nlimsucg  6661  limomss  6689  nnlim  6697  peano5  6707  unielxp  6820  cnvf1o  6882  smoel  7031  smo11  7035  tz7.44-2  7073  oawordeulem  7203  oaordex  7207  omordi  7215  oneo  7230  oeordi  7236  oeoa  7246  oeoe  7248  nnmordi  7280  nnaordex  7287  omabs  7296  nnneo  7300  omsmolem  7302  elqsn0  7380  qsel  7390  mapsn  7460  undifixp  7505  boxriin  7511  boxcutc  7512  fineqvlem  7734  fineqv  7735  pssnn  7738  fissuni  7825  dffi2  7883  inficl  7885  dffi3  7891  wofib  7970  zfregcl  8020  en3lplem1  8031  en3lp  8033  suc11reg  8036  inf0  8038  inf3lem2  8046  inf3lem3  8047  infeq5i  8053  axinf2  8057  dfom3  8064  elom3  8065  noinfepOLD  8077  cantnfle  8090  oemapvali  8103  cantnflem1c  8106  cantnflem1  8108  cantnfleOLD  8120  cantnflem1cOLD  8129  cantnflem1OLD  8131  tc2  8173  r1sdom  8192  rankwflemb  8211  rankval3b  8244  rankunb  8268  rankuni2b  8271  tcrank  8302  cardlim  8353  cardprclem  8360  infxpenlem  8391  alephnbtwn  8452  alephordi  8455  cardaleph  8470  alephfp  8489  alephval3  8491  aceq1  8498  aceq2  8500  dfac3  8502  dfac5lem2  8505  dfac5lem4  8507  dfac2  8511  kmlem2  8531  kmlem4  8533  coflim  8641  cfsmolem  8650  fin23lem30  8722  isf32lem2  8734  isf34lem4  8757  axdc2lem  8828  axdc3lem2  8831  axdc3lem4  8833  axdc4lem  8835  zorn2lem7  8882  axdclem  8899  brdom7disj  8909  brdom6disj  8910  axpowndlem3  8975  axpowndlem3OLD  8976  winainflem  9071  iswun  9082  eltskg  9128  inar1  9153  elgrug  9170  inaprc  9214  eltskm  9221  addnidpi  9279  indpi  9285  nqereu  9307  elnp  9365  elnpi  9366  genpnnp  9383  ltaddpr  9412  dfnn2  10549  dfnn3  10550  dfuzi  10951  uz11  11104  elfzonlteqm1  11859  om2uzlti  12029  axdc4uz  12061  hashrabsn1  12410  hashbclem  12467  hashf1lem2  12471  hash2prd  12484  hash2prv  12491  wrdsymb0  12540  lsw0  12551  rpnnen2lem1  13809  rpnnen2lem2  13810  sadcp1  13964  ismre  14845  isacs  14906  clatl  15603  mreclatBAD  15674  issubm  15797  cycsubg  16034  isnsg  16035  subgacs  16041  nsgacs  16042  resghm  16088  ghmeql  16094  gsmsymgreq  16262  f1otrspeq  16278  pmtrval  16282  pmtrdifellem4  16310  pmtrprfval  16318  gsumzsplit  16747  gsumzsplitOLD  16748  pgpfac1lem1  16927  pgpfac1lem5  16932  pgpfac1  16933  issubrg  17229  islss  17381  lssacs  17413  lspsneq0  17458  lmhmeql  17501  lspdisjb  17572  lidl1el  17665  lidldvgen  17702  0rng01eq  17718  mplcoe1  17926  mplcoe5  17930  mplcoe2OLD  17932  islindf4  18668  m1detdiag  18894  mdetunilem9  18917  maducoeval2  18937  madugsum  18940  chpmat1dlem  19131  istopg  19199  fiinbas  19248  topbas  19268  ppttop  19302  pptbas  19303  epttop  19304  elcls  19368  clsndisj  19370  elcls3  19378  iscldtop  19390  neiptopnei  19427  restbas  19453  restntr  19477  pnfnei  19515  mnfnei  19516  cnpimaex  19551  lmcvg  19557  iscnp4  19558  cncnpi  19573  cnconst2  19578  cnprest  19584  cnprest2  19585  cnpdis  19588  lmss  19593  lmff  19596  cnt0  19641  ist1-3  19644  cnhaus  19649  isreg2  19672  dishaus  19677  ordthauslem  19678  cmpsublem  19693  cmpsub  19694  cmpcld  19696  hauscmplem  19700  bwthOLD  19705  uncon  19724  concompid  19726  concompcon  19727  concompss  19728  1stcfb  19740  1stcrest  19748  2ndcctbss  19750  2ndcomap  19753  dis2ndc  19755  1stcelcls  19756  llyeq  19765  nllyeq  19766  restnlly  19777  restlly  19778  islly2  19779  lly1stc  19791  dislly  19792  hauspwdom  19796  llycmpkgen2  19814  txbas  19831  eltx  19832  ptpjopn  19876  ptclsg  19879  dfac14lem  19881  txcnp  19884  ptcnplem  19885  ptcnp  19886  txlly  19900  pthaus  19902  txtube  19904  txhaus  19911  txlm  19912  tx1stc  19914  txkgen  19916  xkohaus  19917  xkopt  19919  xkococnlem  19923  tgqtop  19976  kqfvima  19994  kqt0lem  20000  isr0  20001  r0cld  20002  regr1lem  20003  kqreglem1  20005  kqreglem2  20006  reghmph  20057  fbssfi  20101  isfil  20111  filuni  20149  isufil  20167  isufil2  20172  uffix  20185  fixufil  20186  uffixfr  20187  uffixsn  20189  rnelfm  20217  flimopn  20239  flimrest  20247  flimcls  20249  flftg  20260  txflf  20270  fclsopni  20279  fclsrest  20288  fclscf  20289  fcfnei  20299  alexsublem  20307  alexsubALTlem3  20312  alexsubALT  20314  tmdgsum2  20358  symgtgp  20363  subgntr  20368  opnsubg  20369  tgpconcompeqg  20373  ghmcnp  20376  tgpt0  20380  divstgpopn  20381  tsmsi  20395  tsmssubm  20407  tsmssplit  20417  isust  20469  ustn0  20486  blssps  20690  blss  20691  blssexps  20692  blssex  20693  neibl  20767  blcld  20771  metss  20774  methaus  20786  met1stc  20787  met2ndci  20788  metrest  20790  prdsxmslem2  20795  metcnp3  20806  dscopn  20857  idnghm  21013  qdensere  21040  tgioo  21064  tgqioo  21068  zdis  21084  xrge0tsms  21102  cnheibor  21218  lmmbr  21460  bcthlem4  21529  ovolicc2lem5  21695  dyadmbllem  21771  i1fd  21851  itg11  21861  itg2gt0  21930  itgeq1f  21941  bddmulibl  22008  ellimc2  22044  limcnlp  22045  ellimc3  22046  limcflf  22048  limciun  22061  lhop1lem  22177  ig1pdvds  22340  plycpn  22447  aannenlem2  22487  efopn  22795  xrlimcnp  23054  wilthlem2  23099  wilthlem3  23100  wilth  23101  tghilbert1_1  23759  tghilbert1_2  23760  colline  23771  lmif  23856  islmib  23858  usgra2edg  24086  usgraedg4  24091  nbgraf1olem1  24145  nbgraf1olem3  24147  nb3graprlem1  24155  nb3graprlem2  24156  uvtx01vtx  24196  uvtxnbgravtx  24199  2trllemF  24255  wlkntrl  24268  constr1trl  24294  eleclclwwlkn  24537  vdgr1a  24610  vdusgra0nedg  24612  usgravd0nedg  24622  eupath2lem1  24681  vdn0frgrav2  24728  vdgn0frgrav2  24729  frgrancvvdeqlem4  24738  frgrancvvdeqlem7  24741  frgrancvvdeqlemA  24742  frgrancvvdeqlemC  24744  frgrawopreg1  24755  frgrawopreg2  24756  lpni  24885  rngoueqz  25136  issh  25829  pjoc1  26056  h1dn0  26174  spansneleqi  26191  nonbooli  26273  pjch  26316  pjnel  26348  cdjreui  27055  rexunirn  27094  rabsnel  27106  opabdm  27165  opabrn  27166  fpwrelmapffslem  27255  fpwrelmap  27256  xrge0tsmsd  27466  tpr2rico  27558  lmxrge0  27598  indval  27695  issiga  27779  isrnsigaOLD  27780  isrnsiga  27781  ddeval1  27874  ddeval0  27875  ddemeas  27876  ismbfm  27891  isanmbfm  27895  dya2icoseg  27916  dya2iocnrect  27920  ballotlem7  28142  erdszelem1  28303  kur14lem9  28326  cnllyscon  28358  cvmcov  28376  cvmsss2  28387  cvmcov2  28388  cvmseu  28389  cvmsiota  28390  cvmopnlem  28391  cvmliftlem15  28411  rtrclreclem.trans  28572  untelirr  28583  untsucf  28585  prodeq1f  28645  dfon2lem4  28823  dfon2lem7  28826  dfon2lem9  28828  soseq  28939  frrlem4  28995  frrlem5e  29000  frrlem11  29004  nodenselem8  29053  nocvxminlem  29055  nofulllem5  29071  dfiota3  29178  funpartlem  29197  funpartfun  29198  tfrqfree  29206  linethru  29408  hilbert1.1  29409  hilbert1.2  29410  rankelg  29430  elhf2  29437  fin2so  29645  heicant  29654  mblfinlem1  29656  ftc1anc  29703  ftc2nc  29704  fneint  29777  finlocfin  29799  locfindis  29805  comppfsc  29807  neibastop2lem  29809  cover2  29835  isbnd2  29910  prdstotbnd  29921  heibor1lem  29936  grpokerinj  29978  isidl  30042  1idl  30054  0rngo  30055  ispridl  30062  smprngopr  30080  isfldidl  30096  isdmn3  30102  iuneq2f  30195  mpt2bi123f  30203  iineq12f  30205  mptbi12f  30207  elmzpcl  30290  diophren  30379  dford3lem2  30601  ttac  30610  pw2f1ocnv  30611  wepwsolem  30619  kelac1  30641  sdrgacs  30783  expgrowthi  30866  dvconstbi  30867  elunif  30997  fnchoice  31010  icccncfext  31254  stoweidlem27  31355  stoweidlem35  31363  stoweidlem46  31374  stoweidlem52  31380  fourierdlem26  31461  funressnfv  31708  fnbrafvb  31734  afvco2  31756  ndmaovg  31764  aovmpt4g  31781  fzoopth  31835  usgpredgv  31894  usgvincvad  31899  usgvincvadALT  31902  usgvad2edg  31906  usg2edgneu  31907  usgedgvadf1lem1  31908  usgedgvadf1lem2  31909  usgedgvadf1ALTlem1  31911  usgedgvadf1ALTlem2  31912  usgedgleord  31914  usgedgleordALT  31915  ldepspr  32173  tratrb  32404  suctrALT2VD  32734  suctrALT2  32735  en3lplem1VD  32741  en3lpVD  32743  tratrbVD  32759  suctrALTcf  32820  suctrALTcfVD  32821  suctrALT3  32822  unisnALT  32824  bnj145OLD  32880  bnj216  32885  bnj563  32897  bnj956  32932  bnj545  33050  bnj548  33052  bnj570  33060  bnj900  33084  bnj929  33091  bnj964  33098  bnj983  33106  bnj1001  33113  bnj1145  33146  bnj1398  33187  bnj1498  33214  bj-rabeqd  33587  bj-cleq  33618  bj-snsetex  33620  bj-nuliota  33685  bj-elopg  33692  lsateln0  33810  ispsubsp  34559  linepsubN  34566  elpcliN  34707  dvh3dim3N  36264  dochsnnz  36265  mapdindp3  36537
  Copyright terms: Public domain W3C validator