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

Theorem eleq2 2672
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 2668 1 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  wcel 1975
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-cleq 2598  df-clel 2601
This theorem is referenced by:  eleq12  2673  eleq2i  2675  nelneq2  2708  dvelimdc  2767  nelne1  2873  raleqf  3106  rexeqf  3107  reueq1f  3108  rmoeq1f  3109  raleleq  3128  rabeqf  3160  clel3g  3305  clel4  3307  sbcbi2  3446  sbcel2gv  3458  csbeq2  3498  difeq2  3679  uneq1  3717  ineq1  3764  unineq  3831  n0i  3874  sbnfc2  3954  disjel  3970  elif  4073  exsnrex  4163  sneqrg  4301  preq1b  4308  preqr1OLD  4311  preq12b  4313  prel12  4314  elpreqprb  4326  elunii  4367  eluniab  4373  ssuniOLD  4386  elinti  4410  elintab  4412  intss1  4417  intmin  4422  intab  4432  iineq2  4464  dfiin2g  4479  breq  4575  zfrepclf  4695  axsep2  4700  zfauscl  4701  sseliALT  4710  inuni  4744  elALT  4828  rext  4833  intid  4843  elopg  4851  opth1  4860  opthwiener  4888  xpeq1  5038  xpeq2  5039  0nelelxp  5055  opthprc  5075  ordtri1  5655  ordtri3  5658  ordtri3OLD  5659  nsuceq0  5704  suctr  5707  suctrOLD  5708  ordnbtwn  5715  ordnbtwnOLD  5716  funopg  5818  dffv2  6162  fveqdmss  6243  dffo4  6264  fnsnb  6311  elunirn  6387  f1oiso  6475  canth  6482  eusvobj2  6516  mpt2eq123  6586  ndmovg  6688  snnex  6835  uniuni  6838  iunpw  6843  oneqmin  6870  onuninsuci  6905  nlimsucg  6907  limomss  6935  nnlim  6943  peano5  6954  unielxp  7068  cnvf1o  7136  smoel  7317  smo11  7321  tz7.44-2  7363  oawordeulem  7494  oaordex  7498  omordi  7506  oneo  7521  oeordi  7527  oeoa  7537  oeoe  7539  nnmordi  7571  nnaordex  7578  omabs  7587  nnneo  7591  omsmolem  7593  elqsn0  7676  qsel  7686  mapsn  7758  undifixp  7803  boxriin  7809  boxcutc  7810  fineqvlem  8032  fineqv  8033  pssnn  8036  fissuni  8127  dffi2  8185  inficl  8187  dffi3  8193  wofib  8306  zfregcl  8355  zfregclOLD  8357  en3lplem1  8367  en3lp  8369  suc11reg  8372  inf0  8374  inf3lem2  8382  inf3lem3  8383  infeq5i  8389  axinf2  8393  dfom3  8400  elom3  8401  cantnfle  8424  oemapvali  8437  cantnflem1c  8440  cantnflem1  8442  tc2  8474  r1sdom  8493  rankwflemb  8512  rankval3b  8545  rankunb  8569  rankuni2b  8572  tcrank  8603  cardlim  8654  cardprclem  8661  infxpenlem  8692  alephnbtwn  8750  alephordi  8753  cardaleph  8768  alephfp  8787  alephval3  8789  aceq1  8796  aceq2  8798  dfac3  8800  dfac5lem2  8803  dfac5lem4  8805  dfac2  8809  kmlem2  8829  kmlem4  8831  coflim  8939  cfsmolem  8948  fin23lem30  9020  isf32lem2  9032  isf34lem4  9055  axdc2lem  9126  axdc3lem2  9129  axdc3lem4  9131  axdc4lem  9133  zorn2lem7  9180  axdclem  9197  brdom7disj  9207  brdom6disj  9208  axpowndlem3  9273  winainflem  9367  iswun  9378  eltskg  9424  inar1  9449  elgrug  9466  inaprc  9510  eltskm  9517  addnidpi  9575  indpi  9581  nqereu  9603  elnp  9661  elnpi  9662  genpnnp  9679  ltaddpr  9708  dfnn2  10876  dfnn3  10877  dfuzi  11296  uz11  11538  elfzonlteqm1  12361  om2uzlti  12562  axdc4uz  12596  hashrabsn1  12972  hashbclem  13041  hashf1lem2  13045  hash2prb  13059  hash2prd  13060  wrdsymb0  13136  lsw0  13147  rtrclreclem3  13590  prodeq1f  14419  rpnnen2lem1  14724  rpnnen2lem2  14725  sadcp1  14957  lcmfval  15114  lcmf0val  15115  ismre  16015  isacs  16077  initoid  16420  termoid  16421  initoeu2lem1  16429  clatl  16881  mreclatBAD  16952  issubm  17112  dfgrp2e  17213  cycsubg  17387  isnsg  17388  subgacs  17394  nsgacs  17395  resghm  17441  ghmeql  17448  gsmsymgreq  17617  f1otrspeq  17632  pmtrval  17636  pmtrdifellem4  17664  pmtrprfval  17672  gsumzsplit  18092  pgpfac1lem1  18238  pgpfac1lem5  18243  pgpfac1  18244  issubrg  18545  lmodfopnelem2  18665  islss  18698  lssacs  18730  lspsneq0  18775  lmhmeql  18818  lspdisjb  18889  lidl1el  18981  lidldvgen  19018  0ring01eq  19034  mplcoe1  19228  mplcoe5  19231  islindf4  19934  m1detdiag  20160  mdetunilem9  20183  maducoeval2  20203  madugsum  20206  chpmat1dlem  20397  istopg  20463  fiinbas  20505  topbas  20525  ppttop  20559  pptbas  20560  epttop  20561  elcls  20625  clsndisj  20627  elcls3  20635  iscldtop  20647  neiptopnei  20684  restbas  20710  restntr  20734  pnfnei  20772  mnfnei  20773  cnpimaex  20808  lmcvg  20814  iscnp4  20815  cncnpi  20830  cnconst2  20835  cnprest  20841  cnprest2  20842  cnpdis  20845  lmss  20850  lmff  20853  cnt0  20898  ist1-3  20901  cnhaus  20906  isreg2  20929  dishaus  20934  ordthauslem  20935  cmpsublem  20950  cmpsub  20951  cmpcld  20953  hauscmplem  20957  uncon  20980  concompid  20982  concompcon  20983  concompss  20984  1stcfb  20996  1stcrest  21004  2ndcctbss  21006  2ndcomap  21009  dis2ndc  21011  1stcelcls  21012  llyeq  21021  nllyeq  21022  restnlly  21033  restlly  21034  islly2  21035  lly1stc  21047  dislly  21048  hauspwdom  21052  finlocfin  21071  unisngl  21078  dissnlocfin  21080  locfindis  21081  comppfsc  21083  llycmpkgen2  21101  txbas  21118  eltx  21119  ptpjopn  21163  ptclsg  21166  dfac14lem  21168  txcnp  21171  ptcnplem  21172  ptcnp  21173  txlly  21187  pthaus  21189  txtube  21191  txhaus  21198  txlm  21199  tx1stc  21201  txkgen  21203  xkohaus  21204  xkopt  21206  xkococnlem  21210  tgqtop  21263  kqfvima  21281  kqt0lem  21287  isr0  21288  r0cld  21289  regr1lem  21290  kqreglem1  21292  kqreglem2  21293  reghmph  21344  fbssfi  21389  isfil  21399  filuni  21437  isufil  21455  isufil2  21460  uffix  21473  fixufil  21474  uffixfr  21475  uffixsn  21477  rnelfm  21505  flimopn  21527  flimrest  21535  flimcls  21537  flftg  21548  txflf  21558  fclsopni  21567  fclsrest  21576  fclscf  21577  fcfnei  21587  alexsublem  21596  alexsubALTlem3  21601  alexsubALT  21603  tmdgsum2  21648  symgtgp  21653  subgntr  21658  opnsubg  21659  tgpconcompeqg  21663  ghmcnp  21666  tgpt0  21670  qustgpopn  21671  tsmsi  21685  tsmssubm  21694  tsmssplit  21703  isust  21755  ustn0  21772  blssps  21976  blss  21977  blssexps  21978  blssex  21979  neibl  22053  blcld  22057  metss  22060  methaus  22072  met1stc  22073  met2ndci  22074  metrest  22076  prdsxmslem2  22081  metcnp3  22092  dscopn  22125  idnghm  22285  qdensere  22311  tgioo  22335  tgqioo  22339  zdis  22355  xrge0tsms  22373  cnheibor  22489  lmmbr  22778  bcthlem4  22845  ovolicc2lem5  23009  dyadmbllem  23086  i1fd  23167  itg11  23177  itg2gt0  23246  itgeq1f  23257  bddmulibl  23324  ellimc2  23360  limcnlp  23361  ellimc3  23362  limcflf  23364  limciun  23377  lhop1lem  23493  ig1pdvds  23653  plycpn  23761  aannenlem2  23801  efopn  24117  xrlimcnp  24408  wilthlem2  24508  wilthlem3  24509  wilth  24510  tghilberti1  25246  tghilberti2  25247  colline  25258  lmif  25391  islmib  25393  usgra2edg  25673  usgraedg4  25678  nbgraf1olem1  25732  nbgraf1olem3  25734  nb3graprlem1  25742  nb3graprlem2  25743  uvtx01vtx  25782  uvtxnbgravtx  25785  2trllemF  25841  wlkntrl  25854  constr1trl  25880  eleclclwwlkn  26122  vdgr1a  26195  vdusgra0nedg  26197  usgravd0nedg  26207  eupath2lem1  26266  vdn0frgrav2  26312  vdgn0frgrav2  26313  frgrancvvdeqlem4  26322  frgrancvvdeqlem7  26325  frgrancvvdeqlemA  26326  frgrancvvdeqlemC  26328  frgrawopreg1  26339  frgrawopreg2  26340  lpni  26484  issh  27251  pjoc1  27479  h1dn0  27597  spansneleqi  27614  nonbooli  27696  pjch  27739  pjnel  27771  cdjreui  28477  rexunirn  28517  rabsnel  28528  opabdm  28605  opabrn  28606  fpwrelmapffslem  28697  fpwrelmap  28698  fz1nntr  28750  xrge0tsmsd  28918  reff  29036  tpr2rico  29088  lmxrge0  29128  indval  29205  issiga  29303  isrnsigaOLD  29304  isrnsiga  29305  isldsys  29348  isros  29360  issros  29367  ddeval1  29426  ddeval0  29427  ddemeas  29428  ismbfm  29443  isanmbfm  29447  dya2icoseg  29468  dya2iocnrect  29472  ballotlem7  29726  bnj145OLD  29851  bnj216  29856  bnj563  29869  bnj956  29903  bnj545  30021  bnj548  30023  bnj570  30031  bnj900  30055  bnj929  30062  bnj964  30069  bnj983  30077  bnj1001  30084  bnj1145  30117  bnj1398  30158  bnj1498  30185  erdszelem1  30229  kur14lem9  30252  cnllyscon  30283  cvmcov  30301  cvmsss2  30312  cvmcov2  30313  cvmseu  30314  cvmsiota  30315  cvmopnlem  30316  cvmliftlem15  30336  mclsssvlem  30515  mclsind  30523  untelirr  30641  untsucf  30643  dfon2lem4  30737  dfon2lem7  30740  dfon2lem9  30742  soseq  30797  frrlem4  30829  frrlem5e  30834  frrlem11  30838  nodenselem8  30889  nocvxminlem  30891  nofulllem5  30907  dfiota3  31002  funpartlem  31021  funpartfun  31022  linethru  31232  hilbert1.1  31233  hilbert1.2  31234  rankelg  31247  elhf2  31254  fneint  31315  neibastop2lem  31327  bj-rabeqd  31907  bj-cleq  31941  bj-snsetex  31943  bj-nuliota  32009  bj-toprntopon  32043  bj-xnex  32044  mptsnunlem  32160  isbasisrelowllem1  32178  isbasisrelowllem2  32179  relowlssretop  32186  relowlpssretop  32187  finxpeq1  32198  finxpreclem5  32207  finxpreclem6  32208  unccur  32361  fin2so  32365  matunitlindflem1  32374  ptrecube  32378  poimirlem9  32387  poimirlem30  32408  poimir  32411  heicant  32413  mblfinlem1  32415  ftc1anc  32462  ftc2nc  32463  cover2  32477  isbnd2  32551  prdstotbnd  32562  heibor1lem  32577  grpokerinj  32661  rngoueqz  32708  isidl  32782  1idl  32794  0rngo  32795  ispridl  32802  smprngopr  32820  isfldidl  32836  isdmn3  32842  mpt2bi123f  32940  iineq12f  32942  mptbi12f  32944  lsateln0  33099  ispsubsp  33848  linepsubN  33855  elpcliN  33996  dvh3dim3N  35555  dochsnnz  35556  mapdindp3  35828  elmzpcl  36106  diophren  36194  dford3lem2  36411  ttac  36420  pw2f1ocnv  36421  wepwsolem  36429  kelac1  36450  sdrgacs  36589  elintabg  36698  elmapintrab  36700  intabssd  36734  eliunov2  36789  gneispaceel2  37261  expgrowthi  37353  dvconstbi  37354  tratrb  37566  suctrALT2VD  37892  suctrALT2  37893  en3lplem1VD  37899  en3lpVD  37901  tratrbVD  37918  suctrALTcf  37979  suctrALTcfVD  37980  suctrALT3  37981  unisnALT  37983  elunif  37997  fnchoice  38010  restuni3  38132  mapsnd  38182  icccncfext  38573  stoweidlem27  38720  stoweidlem35  38728  stoweidlem46  38739  stoweidlem52  38745  ioorrnopnlem  39000  ioorrnopnxrlem  39002  issal  39010  intsaluni  39023  salgencntex  39037  sge0f1o  39075  smfresal  39473  funressnfv  39657  fnbrafvb  39684  afvco2  39706  ndmaovg  39714  aovmpt4g  39731  nnsum4primeseven  40017  nnsum4primesevenALTV  40018  fundmge2nop0  40148  fzoopth  40183  incistruhgr  40303  upgr1eopALT  40340  uhgrvtxedgiedgb  40367  upgredg2vtx  40371  uhgr2edg  40433  umgrvad2edg  40438  umgr2edgneu  40439  usgredg4  40442  usgredg2vtxeuALT  40447  uspgredg2vlem  40448  uspgredg2v  40449  ushgredgedga  40454  usgredgaleordALT  40459  nbgr1vtx  40578  nbusgredgeu0  40594  nbusgrf1o0  40595  nbusgrf1o  40597  nb3grprlem1  40606  nb3grprlem2  40607  uvtxa01vtx0  40621  nbupgruvtxres  40632  cplgr1vlem  40649  cplgr1v  40650  vtxd0nedgb  40701  vtxdushgrfvedglem  40702  vtxduhgr0nedg  40705  1loopgrvd2  40716  1egrvtxdg0  40725  uspgrloopvtxel  40730  1wlk1walk  40841  1wlkp1lem1  40880  pthdivtx  40933  0enwwlksnge1  41058  umgrwwlks2on  41159  rusgr0edg  41174  eleclclwwlksn  41258  upgr4cycl4dv4e  41350  1conngr  41359  vdn0conngrumgrv2  41361  eupth2eucrct  41383  eupth2lem1  41384  frgrncvvdeqlem4  41470  frgrncvvdeqlem7  41473  frgrncvvdeqlemA  41474  frgrncvvdeqlemC  41476  frgrwopreg1  41485  frgrwopreg2  41486  issubmgm  41577  c0snmgmhm  41702  c0snmhm  41703  rngccatidALTV  41779  ringccatidALTV  41842  ldepspr  42054
  Copyright terms: Public domain W3C validator