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

Theorem eleq2 2538
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 2534 1  |-  ( A  =  B  ->  ( C  e.  A  <->  C  e.  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    = wceq 1452    e. wcel 1904
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672  df-cleq 2464  df-clel 2467
This theorem is referenced by:  eleq12  2539  eleq2i  2541  nelneq2  2574  dvelimdc  2633  nelne1  2739  raleqf  2969  rexeqf  2970  reueq1f  2971  rmoeq1f  2972  raleleq  2991  rabeqf  3023  clel3g  3164  clel4  3166  sbcbi2  3304  sbcel2gv  3315  csbeq2  3353  difeq2  3534  uneq1  3572  ineq1  3618  unineq  3684  n0i  3727  sbnfc2  3800  disjel  3815  elif  3912  exsnrex  4000  sneqr  4131  preq1b  4137  preqr1OLD  4140  preq12b  4142  prel12  4143  elpreqprb  4154  elunii  4195  eluniab  4201  ssuni  4212  elinti  4235  elintab  4237  intss1  4241  intmin  4246  intab  4256  iineq2  4287  dfiin2g  4302  breq  4397  zfrepclf  4514  axsep2  4519  zfauscl  4520  sseliALT  4529  inuni  4563  pwne0  4571  elALT  4643  rext  4648  intid  4658  elopg  4666  opth1  4675  opthwiener  4703  xpeq1  4853  xpeq2  4854  opthprc  4887  ordtri1  5463  ordtri3  5466  nsuceq0  5510  suctr  5513  ordnbtwn  5520  funopg  5621  dffv2  5953  fveqdmss  6032  dffo4  6053  fnsnb  6099  elunirn  6174  f1oiso  6260  canth  6267  eusvobj2  6301  mpt2eq123  6369  ndmovg  6471  snnex  6616  uniuni  6619  iunpw  6624  oneqmin  6651  onuninsuci  6686  nlimsucg  6688  limomss  6716  nnlim  6724  peano5  6735  unielxp  6848  cnvf1o  6914  smoel  7097  smo11  7101  tz7.44-2  7143  oawordeulem  7273  oaordex  7277  omordi  7285  oneo  7300  oeordi  7306  oeoa  7316  oeoe  7318  nnmordi  7350  nnaordex  7357  omabs  7366  nnneo  7370  omsmolem  7372  elqsn0  7450  qsel  7460  mapsn  7531  undifixp  7576  boxriin  7582  boxcutc  7583  fineqvlem  7804  fineqv  7805  pssnn  7808  fissuni  7897  dffi2  7955  inficl  7957  dffi3  7963  wofib  8078  zfregcl  8127  en3lplem1  8137  en3lp  8139  suc11reg  8142  inf0  8144  inf3lem2  8152  inf3lem3  8153  infeq5i  8159  axinf2  8163  dfom3  8170  elom3  8171  cantnfle  8194  oemapvali  8207  cantnflem1c  8210  cantnflem1  8212  tc2  8244  r1sdom  8263  rankwflemb  8282  rankval3b  8315  rankunb  8339  rankuni2b  8342  tcrank  8373  cardlim  8424  cardprclem  8431  infxpenlem  8462  alephnbtwn  8520  alephordi  8523  cardaleph  8538  alephfp  8557  alephval3  8559  aceq1  8566  aceq2  8568  dfac3  8570  dfac5lem2  8573  dfac5lem4  8575  dfac2  8579  kmlem2  8599  kmlem4  8601  coflim  8709  cfsmolem  8718  fin23lem30  8790  isf32lem2  8802  isf34lem4  8825  axdc2lem  8896  axdc3lem2  8899  axdc3lem4  8901  axdc4lem  8903  zorn2lem7  8950  axdclem  8967  brdom7disj  8977  brdom6disj  8978  axpowndlem3  9042  winainflem  9136  iswun  9147  eltskg  9193  inar1  9218  elgrug  9235  inaprc  9279  eltskm  9286  addnidpi  9344  indpi  9350  nqereu  9372  elnp  9430  elnpi  9431  genpnnp  9448  ltaddpr  9477  dfnn2  10644  dfnn3  10645  dfuzi  11049  uz11  11205  elfzonlteqm1  12018  om2uzlti  12202  axdc4uz  12234  hashrabsn1  12591  hashbclem  12656  hashf1lem2  12660  hash2prb  12674  hash2prd  12675  wrdsymb0  12752  lsw0  12763  rtrclreclem3  13200  prodeq1f  14039  rpnnen2lem1  14344  rpnnen2lem2  14345  sadcp1  14508  lcmfval  14670  lcmf0val  14671  lcmfvalOLD  14674  ismre  15574  isacs  15635  initoid  15978  termoid  15979  initoeu2lem1  15987  clatl  16440  mreclatBAD  16511  issubm  16672  cycsubg  16923  isnsg  16924  subgacs  16930  nsgacs  16931  resghm  16977  ghmeql  16983  gsmsymgreq  17151  f1otrspeq  17166  pmtrval  17170  pmtrdifellem4  17198  pmtrprfval  17206  gsumzsplit  17638  pgpfac1lem1  17785  pgpfac1lem5  17790  pgpfac1  17791  issubrg  18086  islss  18236  lssacs  18268  lspsneq0  18313  lmhmeql  18356  lspdisjb  18427  lidl1el  18519  lidldvgen  18556  0ring01eq  18572  mplcoe1  18766  mplcoe5  18769  islindf4  19473  m1detdiag  19699  mdetunilem9  19722  maducoeval2  19742  madugsum  19745  chpmat1dlem  19936  istopg  20002  fiinbas  20044  topbas  20065  ppttop  20099  pptbas  20100  epttop  20101  elcls  20166  clsndisj  20168  elcls3  20176  iscldtop  20188  neiptopnei  20225  restbas  20251  restntr  20275  pnfnei  20313  mnfnei  20314  cnpimaex  20349  lmcvg  20355  iscnp4  20356  cncnpi  20371  cnconst2  20376  cnprest  20382  cnprest2  20383  cnpdis  20386  lmss  20391  lmff  20394  cnt0  20439  ist1-3  20442  cnhaus  20447  isreg2  20470  dishaus  20475  ordthauslem  20476  cmpsublem  20491  cmpsub  20492  cmpcld  20494  hauscmplem  20498  uncon  20521  concompid  20523  concompcon  20524  concompss  20525  1stcfb  20537  1stcrest  20545  2ndcctbss  20547  2ndcomap  20550  dis2ndc  20552  1stcelcls  20553  llyeq  20562  nllyeq  20563  restnlly  20574  restlly  20575  islly2  20576  lly1stc  20588  dislly  20589  hauspwdom  20593  finlocfin  20612  unisngl  20619  dissnlocfin  20621  locfindis  20622  comppfsc  20624  llycmpkgen2  20642  txbas  20659  eltx  20660  ptpjopn  20704  ptclsg  20707  dfac14lem  20709  txcnp  20712  ptcnplem  20713  ptcnp  20714  txlly  20728  pthaus  20730  txtube  20732  txhaus  20739  txlm  20740  tx1stc  20742  txkgen  20744  xkohaus  20745  xkopt  20747  xkococnlem  20751  tgqtop  20804  kqfvima  20822  kqt0lem  20828  isr0  20829  r0cld  20830  regr1lem  20831  kqreglem1  20833  kqreglem2  20834  reghmph  20885  fbssfi  20930  isfil  20940  filuni  20978  isufil  20996  isufil2  21001  uffix  21014  fixufil  21015  uffixfr  21016  uffixsn  21018  rnelfm  21046  flimopn  21068  flimrest  21076  flimcls  21078  flftg  21089  txflf  21099  fclsopni  21108  fclsrest  21117  fclscf  21118  fcfnei  21128  alexsublem  21137  alexsubALTlem3  21142  alexsubALT  21144  tmdgsum2  21189  symgtgp  21194  subgntr  21199  opnsubg  21200  tgpconcompeqg  21204  ghmcnp  21207  tgpt0  21211  qustgpopn  21212  tsmsi  21226  tsmssubm  21235  tsmssplit  21244  isust  21296  ustn0  21313  blssps  21517  blss  21518  blssexps  21519  blssex  21520  neibl  21594  blcld  21598  metss  21601  methaus  21613  met1stc  21614  met2ndci  21615  metrest  21617  prdsxmslem2  21622  metcnp3  21633  dscopn  21666  idnghm  21842  qdensere  21868  tgioo  21892  tgqioo  21896  zdis  21912  xrge0tsms  21930  cnheibor  22061  lmmbr  22306  bcthlem4  22373  ovolicc2lem5  22553  dyadmbllem  22636  i1fd  22718  itg11  22728  itg2gt0  22797  itgeq1f  22808  bddmulibl  22875  ellimc2  22911  limcnlp  22912  ellimc3  22913  limcflf  22915  limciun  22928  lhop1lem  23044  ig1pdvds  23207  ig1pdvdsOLD  23213  plycpn  23321  aannenlem2  23364  efopn  23682  xrlimcnp  23973  wilthlem2  24073  wilthlem3  24074  wilth  24075  tghilberti1  24761  tghilberti2  24762  colline  24773  lmif  24906  islmib  24908  usgra2edg  25188  usgraedg4  25193  nbgraf1olem1  25248  nbgraf1olem3  25250  nb3graprlem1  25258  nb3graprlem2  25259  uvtx01vtx  25299  uvtxnbgravtx  25302  2trllemF  25358  wlkntrl  25371  constr1trl  25397  eleclclwwlkn  25640  vdgr1a  25713  vdusgra0nedg  25715  usgravd0nedg  25725  eupath2lem1  25784  vdn0frgrav2  25830  vdgn0frgrav2  25831  frgrancvvdeqlem4  25840  frgrancvvdeqlem7  25843  frgrancvvdeqlemA  25844  frgrancvvdeqlemC  25846  frgrawopreg1  25857  frgrawopreg2  25858  lpni  25990  rngoueqz  26239  issh  26942  pjoc1  27168  h1dn0  27286  spansneleqi  27303  nonbooli  27385  pjch  27428  pjnel  27460  cdjreui  28166  rexunirn  28206  rabsnel  28217  opabdm  28295  opabrn  28296  fpwrelmapffslem  28392  fpwrelmap  28393  fz1nntr  28453  xrge0tsmsd  28622  reff  28740  tpr2rico  28792  lmxrge0  28832  indval  28909  issiga  29007  isrnsigaOLD  29008  isrnsiga  29009  isldsys  29052  isros  29064  issros  29071  ddeval1  29130  ddeval0  29131  ddemeas  29132  ismbfm  29147  isanmbfm  29151  dya2icoseg  29172  dya2iocnrect  29176  ballotlem7  29441  ballotlem7OLD  29479  bnj145OLD  29607  bnj216  29612  bnj563  29625  bnj956  29660  bnj545  29778  bnj548  29780  bnj570  29788  bnj900  29812  bnj929  29819  bnj964  29826  bnj983  29834  bnj1001  29841  bnj1145  29874  bnj1398  29915  bnj1498  29942  erdszelem1  29986  kur14lem9  30009  cnllyscon  30040  cvmcov  30058  cvmsss2  30069  cvmcov2  30070  cvmseu  30071  cvmsiota  30072  cvmopnlem  30073  cvmliftlem15  30093  mclsssvlem  30272  mclsind  30280  untelirr  30407  untsucf  30409  dfon2lem4  30503  dfon2lem7  30506  dfon2lem9  30508  soseq  30563  frrlem4  30588  frrlem5e  30593  frrlem11  30597  nodenselem8  30648  nocvxminlem  30650  nofulllem5  30666  dfiota3  30761  funpartlem  30780  funpartfun  30781  linethru  30991  hilbert1.1  30992  hilbert1.2  30993  rankelg  31006  elhf2  31013  fneint  31075  neibastop2lem  31087  bj-rabeqd  31591  bj-cleq  31625  bj-snsetex  31627  bj-nuliota  31693  mptsnunlem  31810  isbasisrelowllem1  31828  isbasisrelowllem2  31829  relowlssretop  31836  relowlpssretop  31837  finxpeq1  31848  finxpreclem5  31857  finxpreclem6  31858  fin2so  31996  ptrecube  32004  poimirlem9  32013  poimirlem30  32034  poimir  32037  heicant  32039  mblfinlem1  32041  ftc1anc  32089  ftc2nc  32090  cover2  32104  isbnd2  32179  prdstotbnd  32190  heibor1lem  32205  grpokerinj  32247  isidl  32311  1idl  32323  0rngo  32324  ispridl  32331  smprngopr  32349  isfldidl  32365  isdmn3  32371  mpt2bi123f  32470  iineq12f  32472  mptbi12f  32474  lsateln0  32632  ispsubsp  33381  linepsubN  33388  elpcliN  33529  dvh3dim3N  35088  dochsnnz  35089  mapdindp3  35361  elmzpcl  35639  diophren  35727  dford3lem2  35953  ttac  35962  pw2f1ocnv  35963  wepwsolem  35971  kelac1  35992  sdrgacs  36138  elintabg  36251  elmapintrab  36253  intabssd  36287  eliunov2  36342  expgrowthi  36752  dvconstbi  36753  tratrb  36967  suctrALT2VD  37295  suctrALT2  37296  en3lplem1VD  37302  en3lpVD  37304  tratrbVD  37321  suctrALTcf  37382  suctrALTcfVD  37383  suctrALT3  37384  unisnALT  37386  elunif  37400  fnchoice  37413  mapsnd  37547  icccncfext  37862  stoweidlem27  37999  stoweidlem35  38008  stoweidlem46  38019  stoweidlem52  38025  issal  38287  intsaluni  38300  salgencntex  38314  sge0f1o  38338  funressnfv  38774  fnbrafvb  38801  afvco2  38823  ndmaovg  38831  aovmpt4g  38848  nnsum4primeseven  39040  nnsum4primesevenALTV  39041  fundmge2nop  39172  fzoopth  39208  incistruhgr  39325  upgr1eopALT  39362  uhgrvtxedgiedgb  39388  upgredg2vtx  39392  uhgr2edg  39453  usgredg4  39458  usgredg2vtxeuALT  39463  uspgredg2vlem  39464  uspgredg2v  39465  ushgredgedga  39470  usgredgaleordALT  39475  usgr1vr  39493  nbgr1vtx  39590  nbusgredgeu0  39606  nbusgrf1o0  39607  nbusgrf1o  39609  nb3grprlem1  39618  nb3grprlem2  39619  uvtxa01vtx0  39633  nbupgruvtxres  39644  cplgr1vlem  39661  cplgr1v  39662  vtxd0nedgb  39711  vtxdushgrfvedglem  39712  vtxduhgr0nedg  39715  1loopgrvd2  39725  1egrvtxdg0  39734  uspgrloopvtxel  39739  1wlk1walk  39838  1wlkp1lem1  39869  pthdivtx  39922  upgr4cycl4dv4e  40099  1conngr  40108  eupth2eucrct  40129  eupth2lem1  40130  usgpredgv  40219  usgvincvad  40224  usgvincvadALT  40227  usgvad2edg  40231  usg2edgneu  40232  usgedgvadf1lem1  40233  usgedgvadf1lem2  40234  usgedgvadf1ALTlem1  40236  usgedgvadf1ALTlem2  40237  usgedgleord  40239  usgedgleordALT  40240  issubmgm  40297  c0snmgmhm  40422  c0snmhm  40423  rngccatidALTV  40499  ringccatidALTV  40562  ldepspr  40774
  Copyright terms: Public domain W3C validator