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

Theorem eleq2d 2502
Description: Deduction from equality to equivalence of membership. (Contributed by NM, 27-Dec-1993.)
Hypothesis
Ref Expression
eleq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
eleq2d  |-  ( ph  ->  ( C  e.  A  <->  C  e.  B ) )

Proof of Theorem eleq2d
StepHypRef Expression
1 eleq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 eleq2 2496 . 2  |-  ( A  =  B  ->  ( C  e.  A  <->  C  e.  B ) )
31, 2syl 16 1  |-  ( ph  ->  ( C  e.  A  <->  C  e.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1652    e. wcel 1725
This theorem is referenced by:  eleq12d  2503  eleqtrd  2511  neleqtrd  2530  neleqtrrd  2531  abeq2d  2544  nfceqdf  2570  drnfc1  2587  drnfc2  2588  sbcbid  3206  cbvcsb  3247  sbcel1g  3262  csbeq2d  3267  csbie2g  3289  cbvralcsf  3303  cbvreucsf  3305  cbvrabcsf  3306  cbviun  4120  cbviin  4121  iinxsng  4159  iinxprg  4160  iunxsng  4161  cbvdisj  4184  disjor  4188  mpteq12f  4277  axpweq  4368  rabxfrd  4735  0nelelxp  4898  opeliunxp  4920  opeliunxp2  5004  iunxpf  5012  elrelimasn  5219  elimasng  5221  elimasni  5222  ressn  5399  funfni  5536  fnbr  5538  fun11iun  5686  dffv3  5715  fvelrnb  5765  fvun1  5785  fvco2  5789  elpreima  5841  dff3  5873  fmptco  5892  fnpr  5941  fnprOLD  5942  zfrep6  5959  funfvima3  5966  eluniima  5988  dff13  5995  f1eqcocnv  6019  isoini  6049  mpt2eq123dva  6126  cbvmpt2x  6141  ovelrn  6213  elovmpt2  6282  fmpt2x  6408  bropopvvv  6417  mpt2xopn0yelv  6455  mpt2xopovel  6462  isprmpt2  6468  rntpos  6483  riotaeqdv  6541  onoviun  6596  smoel  6613  smoiso  6615  smoel2  6616  smo11  6617  tfrlem9  6637  oalimcl  6794  oaass  6795  omordi  6800  omordlim  6811  omlimcl  6812  odi  6813  omeulem1  6816  omeulem2  6817  oen0  6820  oeordi  6821  oeordsuc  6828  oelimcl  6834  oeeulem  6835  oeeui  6836  nnmordi  6865  oaabs2  6879  omabs  6881  omsmolem  6887  ereldm  6939  iiner  6967  elmapg  7022  elpmg  7023  elixpsn  7092  ixpsnf1o  7093  boxriin  7095  omxpenlem  7200  pw2f1olem  7203  phplem4  7280  php3  7284  elfi  7409  dffi3  7427  marypha2lem2  7432  ordiso2  7473  wemapso2lem  7508  elharval  7520  inf3lemd  7571  inf3lem1  7572  inf3lem2  7573  inf3lem3  7574  cantnfs  7610  cantnfp1lem3  7625  cantnflem1b  7631  cantnflem1  7634  trcl  7653  r1sdom  7689  r1ordg  7693  r1pwss  7699  tz9.12lem3  7704  tz9.12  7705  r1elwf  7711  rankr1ai  7713  rankidb  7715  rankr1bg  7718  rankval2  7733  rankunb  7765  tcrank  7797  fseqdom  7896  acni  7915  acni2  7916  acndom  7921  infpwfien  7932  alephnbtwn  7941  cardaleph  7959  cardinfima  7967  iunfictbso  7984  dfac3  7991  dfac5lem5  7997  dfac5  7998  dfac9  8005  dfac12r  8015  kmlem2  8020  kmlem12  8030  kmlem13  8031  kmlem14  8032  ackbij2lem3  8110  ackbij2  8112  cofsmo  8138  cfsmolem  8139  alephsing  8145  fin23lem30  8211  isf32lem9  8230  itunisuc  8288  axcc2lem  8305  axcc3  8307  domtriomlem  8311  axdc2lem  8317  axdc2  8318  axdc3lem2  8320  axdc3lem4  8322  axdc4lem  8324  ac6c4  8350  zorn2lem1  8365  ttukeylem6  8383  pwcfsdom  8447  axregndlem2  8467  axinfndlem1  8469  axacndlem4  8474  axacnd  8476  pwfseqlem1  8522  inar1  8639  inatsk  8642  gruurn  8662  grur1  8684  grothpw  8690  eltskm  8707  genpelv  8866  eluz1  10481  eluzadd  10503  eluzsub  10504  elixx1  10914  elixx3g  10918  elioo2  10946  elfz1  11037  elfz2  11039  elfzp1  11086  fzpr  11090  fzsuc2  11093  fzrev3  11100  elfzp12  11114  elfzo  11130  elfzom1b  11179  fzosplitsni  11184  seqp1  11326  seqf1o  11352  bcval  11583  bcpasc  11600  hashf1lem1  11692  ccatfval  11730  ccatlid  11736  ccatass  11738  swrdid  11760  ccatswrd  11761  swrdccat2  11763  cats1un  11778  revccat  11786  revrev  11787  revco  11791  ccatco  11792  shftfn  11876  shftval  11877  limsupgle  12259  ello12  12298  elo12  12309  isercolllem3  12448  sumeq1f  12470  fsumsplit  12521  sumsplit  12540  fsum2dlem  12542  fsumcom2  12546  fsumparts  12573  explecnv  12632  eftlub  12698  divalgmod  12914  bitsval  12924  bitsp1e  12932  bitsp1o  12933  sadfval  12952  sadcp1  12955  sadval  12956  sadcadd  12958  sadadd2  12960  saddisjlem  12964  sadadd  12967  sadass  12971  smufval  12977  smuval  12981  smuval2  12982  smupvallem  12983  smu01lem  12985  smueqlem  12990  smumul  12993  bezoutlem2  13027  bezoutlem4  13029  algfx  13059  eucalgcvga  13065  unbenlem  13264  prmreclem5  13276  vdwapval  13329  vdwapun  13330  vdwnnlem1  13351  vdwnn  13354  ramval  13364  0ram  13376  ramub1lem2  13383  prmlem0  13416  elrest  13643  prdsbasmpt  13680  prdsleval  13687  prdsbasmpt2  13692  pwselbasb  13698  imasaddfnlem  13741  imasvscafn  13750  divsfval  13760  ismre  13803  mreunirn  13814  mrisval  13843  ismri  13844  isacs  13864  catidd  13893  iscatd2  13894  ismon  13947  isepi  13954  sectffval  13964  sectfval  13965  issubc  14023  isfunc  14049  funcres  14081  funcpropd  14085  ffthiso  14114  isnat  14132  isnat2  14133  fuciso  14160  arwhoma  14188  elsetchom  14224  setcmon  14230  setcepi  14231  setciso  14234  catciso  14250  hofcl  14344  hofpropd  14352  yonedalem4c  14362  yonedainv  14366  yonffthlem  14367  poslubdg  14563  acsficl2d  14590  acsmapd  14592  psref  14628  psss  14634  dirge  14670  grpidval  14695  grpidd  14706  ismndd  14707  mndpropd  14709  grpidpropd  14710  imasmnd2  14720  imasmnd  14721  ismhm  14728  issubm  14736  gsumccat  14775  imasgrp2  14921  imasgrp  14922  issubg  14932  subginv  14939  isnsg  14957  isghm  14994  resghm2b  15012  conjnmzb  15028  conjnsg  15029  ghmpropd  15031  isga  15056  elcntz  15109  elcntzsn  15112  cntzrcl  15114  resscntz  15118  gexdvds  15206  gex1  15213  isslw  15230  sylow3lem2  15250  lsmelvalx  15262  pj1ghm  15323  efgtlen  15346  efgs1b  15356  efgsfo  15359  efgredlemc  15365  frgp0  15380  frgpmhm  15385  divsabl  15468  frgpnabllem1  15472  0cyg  15490  cycsubgcyg  15498  gsumval3  15502  gsumcllem  15504  gsumzaddlem  15514  gsumzsplit  15517  eldprd  15550  dprdcntz2  15584  dprd2d2  15590  dmdprdsplit2lem  15591  dmdprdsplit2  15592  dprdsplit  15594  ablfac2  15635  isrngd  15686  imasrng  15713  dvdsrval  15738  isunit  15750  dvdsrpropd  15789  isirred  15792  isrhm  15812  drngunit  15828  isdrngd  15848  issubrg  15856  opprsubrg  15877  rhmpropd  15891  isabv  15895  issrngd  15937  islmod  15942  lmodprop2d  15994  islss  15999  islssd  16000  lssats2  16064  lspsnel  16067  islmhm  16091  lmhmf1o  16110  lmhmima  16111  lmhmpreima  16112  reslmhm  16116  lmhmpropd  16133  islbs  16136  lspprel  16154  lspfixed  16188  lbsacsbs  16216  lbsextlem1  16218  lbsextlem2  16219  lbsextlem3  16220  lbsextlem4  16221  lidlmcl  16276  divscrng  16299  islpidl  16305  lidldvgen  16314  mplsubglem  16486  mpllsslem  16487  mplmonmul  16515  mplrcl  16538  subrgascl  16546  subrgasclcl  16547  strov2rcl  16619  zrhrhmb  16780  znf1o  16820  frgpcyg  16842  isphld  16873  elocv  16883  iscss  16898  isobs  16935  obs2ss  16944  istopon  16978  eltg  17010  eltg2  17011  eltop  17027  eltop2  17028  eltop3  17029  pptbas  17060  iscld  17079  neiss2  17153  isnei  17155  neiptopnei  17184  neiptopreu  17185  lpfval  17190  lpval  17191  islp  17192  maxlp  17199  islpi  17201  neitr  17232  restlp  17235  ordtbas2  17243  ordtrest2  17256  lmfval  17284  cnfval  17285  iscn  17287  iscnp  17289  tgcn  17304  tgcnp  17305  lmbrf  17312  cnpresti  17340  ist1  17373  ist1-2  17399  cnt1  17402  haust1  17404  cmpfi  17459  cmpfii  17460  1stcfb  17496  2ndc1stc  17502  1stcrest  17504  2ndcdisj  17507  1stcelcls  17512  nllyi  17526  subislly  17532  kgenval  17555  elkgen  17556  kgencn2  17577  txbas  17587  eltx  17588  ptval  17590  ptpjpre1  17591  ptopn2  17604  ptpjopn  17632  ptclsg  17635  xkoccn  17639  txdis  17652  txdis1cn  17655  ptrescn  17659  hausdiag  17665  hauseqlcld  17666  txhaus  17667  xkohaus  17673  elqtop  17717  qtopeu  17736  kqcldsat  17753  hmeofval  17778  ptuncnv  17827  ptunhmeo  17828  elmptrab  17847  fbdmn0  17854  elfg  17891  elfilss  17896  filunirn  17902  fixufil  17942  elfm  17967  rnelfmlem  17972  rnelfm  17973  fmfnfmlem4  17977  elflim2  17984  flimtopon  17990  elflim  17991  hausflim  18001  flimcls  18005  flfnei  18011  isflf  18013  hausflf  18017  cnpflf  18021  cnflf  18022  txflf  18026  isfcls  18029  fclstopon  18032  isfcls2  18033  fclssscls  18038  fclsnei  18039  fclsfnflim  18047  flimfnfcls  18048  isfcf  18054  fcfelbas  18056  cnpfcf  18061  cnfcf  18062  alexsublem  18063  alexsubALTlem3  18068  cnextfun  18083  cnextfvval  18084  cnextf  18085  cnextcn  18086  tmdgsum2  18114  tgpconcomp  18130  ghmcnp  18132  divstgplem  18138  eltsms  18150  haustsms  18153  tsmsgsum  18156  tsmssubm  18160  tsmssplit  18169  isust  18221  elrnust  18242  ustbas  18245  elutop  18251  ustuqtoplem  18257  ustuqtop4  18262  ustuqtop  18264  utopsnneiplem  18265  utopsnneip  18266  utopsnnei  18267  isusp  18279  isucn  18296  ucncn  18303  iscfilu  18306  neipcfilu  18314  iscusp  18317  cnextucn  18321  ispsmet  18323  ismet  18341  isxmet  18342  elblps  18405  elbl  18406  elmopn  18460  prdsbl  18509  neibl  18519  met1stc  18539  metrest  18542  prdsxmslem2  18547  txmetcnp  18565  txmetcn  18566  metuvalOLD  18567  metuval  18568  metustsymOLD  18579  metustsym  18580  cfilucfil2OLD  18591  cfilucfil2  18592  elbl4  18594  metuelOLD  18595  metuel  18596  metutopOLD  18600  psmetutop  18601  restmetu  18605  metucnOLD  18606  metucn  18607  tngngp  18683  isnmhm  18768  zcld  18832  metnrmlem1a  18876  elcncf  18907  cncfcnvcn  18939  cnheibor  18968  lebnumlem1  18974  ishtpy  18985  isphtpy  18994  om1elbas  19045  elpi1  19058  pi1xfr  19068  pi1coghm  19074  tchcph  19182  lmmbrf  19203  iscfil  19206  iscau  19217  iscauf  19221  caucfil  19224  iscmet  19225  cmetcaulem  19229  iscmet3lem1  19232  iscmet3lem2  19233  iscmet3  19234  bcthlem1  19265  cmsss  19291  cmetcusp1OLD  19293  cmetcusp1  19294  cmetcuspOLD  19295  cmetcusp  19296  minveclem3b  19317  ovolfioo  19352  ovolficc  19353  ovolctb  19374  ovoliunnul  19391  ovolshftlem1  19393  sca2rab  19396  ovolscalem1  19397  ovolicc2lem1  19401  ovolicc2lem2  19402  ovolicc2lem4  19404  ovolicc2lem5  19405  iundisj  19430  iunmbl2  19439  uniioombllem3  19465  vitalilem2  19489  vitalilem3  19490  mbfss  19526  i1faddlem  19573  i1fmullem  19574  mbfi1fseqlem2  19596  mbfi1fseqlem4  19598  mbfi1fseq  19601  itg2splitlem  19628  itg2split  19629  itg2monolem1  19630  itg2gt0  19640  isibl  19645  iblss2  19685  itgss3  19694  itgsplit  19715  ellimc  19748  limcmo  19757  cnlimc  19763  limciun  19769  limcun  19770  eldv  19773  dvbsss  19777  dvreslem  19784  elcpn  19808  dvaddf  19816  dvmulf  19817  dvcof  19822  rolle  19862  dvlip2  19867  dvivthlem1  19880  lhop1  19886  lhop2  19887  ftc1cn  19915  mpfind  19953  fta1glem2  20077  plyco0  20099  elply  20102  ply1termlem  20110  eltayl  20264  tayl0  20266  taylplem1  20267  taylplem2  20268  dvtaylp  20274  taylthlem1  20277  taylthlem2  20278  abelth  20345  cxpcn3  20620  rlimcnp  20792  fsumharmonic  20838  dchrelbas  21008  pntrsumbnd2  21249  ostth2lem2  21316  usgra2edg1  21391  usgraidx2vlem1  21398  usgraidx2vlem2  21399  nbgraop  21424  nbgrael  21426  nbgraeledg  21430  nbgraf1olem1  21439  nbgraf1olem3  21441  nbgraf1olem5  21443  nbgraf1o  21445  iscusgra  21453  sizeusglecusglem1  21481  isuvtx  21485  uvtxel  21486  uvtxisvtx  21487  wlks  21514  iswlk  21515  istrl  21525  ispth  21556  isspth  21557  fargshiftlem  21609  fargshiftfv  21610  fargshiftfo  21613  vdgrfval  21654  vdgrun  21660  vdgrfiun  21661  vdgr1a  21665  eupap1  21686  eupath2lem3  21689  ex-res  21737  isabloda  21875  issubgo  21879  isass  21892  elghomlem2  21938  ghablo  21945  iscom2  21988  rngoidmlem  21999  rngo1cl  22005  isssp  22211  sspn  22223  islno  22242  isblo  22271  nmlno0  22284  ishmo  22300  dipdir  22331  dipass  22334  ubthlem1  22360  ubthlem2  22361  htthlem  22408  htth  22409  ocel  22771  ocnel  22788  shsel  22804  shsel2  22812  shmodsi  22879  pjhtheu  22884  pjeq  22889  axpjpj  22910  pjoc2  22929  elspani  23033  h1de2ctlem  23045  elspansn  23056  elspansn2  23057  elnlfn  23419  eleigvec  23448  riesz3i  23553  iuneq12daf  23995  iuneq12df  23996  iunrdx  24002  cbvdisjf  24003  disjorf  24009  disjabrex  24012  disjabrexf  24013  iundisjf  24017  disjrdx  24019  elunirn2  24051  abfmpunirn  24052  abfmpeld  24054  abfmpel  24055  fmptdF  24057  fmptcof2  24064  funcnvmptOLD  24070  funcnvmpt  24071  xrofsup  24114  iundisjfi  24140  eliccioo  24165  xrge0tsmsbi  24212  inftmrel  24238  isinftm  24239  metidval  24273  pstmval  24278  cnre2csqima  24297  fmcncfil  24305  ofcfval  24469  measvuni  24556  meascnbl  24561  faeval  24585  ismbfm  24590  elunirnmbfm  24591  isanmbfm  24594  imambfm  24600  itgeq12dv  24629  issibf  24636  rrvmbfm  24688  elorvc  24705  elorrvc  24709  dstfrvunirn  24720  ballotlemfc0  24738  ballotlemfcc  24739  ballotlemsima  24761  ballotlemrv  24765  subfacp1lem2b  24855  subfacp1lem4  24857  subfacp1lem5  24858  subfacp1lem6  24859  ptpcon  24908  cvmscbv  24933  iscvm  24934  cvmsi  24940  cvmsval  24941  cvmliftmolem1  24956  cvmlift2lem12  24989  cvmlift2lem13  24990  cvmlift3lem7  25000  snmlval  25006  elgiso  25095  fprodser  25264  fprodsplit  25278  fprod2dlem  25293  fprodcom2  25297  mpteq12d  25383  predbrg  25441  trpredrec  25496  wfrlem9  25519  wfrlem12  25522  fvnobday  25591  nodenselem3  25592  nodenselem5  25594  nofulllem5  25615  elee  25781  brbtwn  25786  brcgr  25787  axlowdimlem16  25844  funtransport  25913  fvtransport  25914  brcolinear  25941  colineardim1  25943  funray  26022  fvray  26023  funline  26024  fvline  26026  lineelsb2  26030  rankelg  26057  rankeq1o  26060  elhf2  26064  0hf  26066  mblfinlem  26190  volsupnfl  26197  itg2addnclem  26202  itg2gt0cn  26206  islocfin  26313  lfinpfin  26320  locfindis  26322  locfincf  26323  comppfsc  26324  neibastop2lem  26326  neibastop3  26328  eltail  26340  indexdom  26373  incsequz  26389  istotbnd  26415  istotbnd3  26417  0totbnd  26419  sstotbnd  26421  sstotbnd3  26422  isbnd  26426  prdstotbnd  26440  cntotbnd  26442  isismty  26447  heibor1lem  26455  heiborlem2  26458  heiborlem3  26459  heibor  26467  exidcl  26488  exidreslem  26489  divrngcl  26510  isdrngo2  26511  isrngohom  26518  isrngoiso  26531  isriscg  26537  iscringd  26546  isidl  26561  ispridl  26581  ismaxidl  26587  prter3  26668  fnelfp  26673  fnelnfp  26675  isnacs  26695  mrefg2  26698  elmzpcl  26720  mzpcompact2  26746  eldiophb  26752  elpell1qr  26847  elpell14qr  26849  elpell1234qr  26851  pw2f1ocnv  27045  pw2f1o2val2  27048  aomclem4  27069  aomclem6  27071  islssfg2  27084  pwssplit3  27105  dsmmbas2  27118  dsmmfi  27119  dsmmelbas  27120  dsmmlss  27125  frlmelbas  27139  frlmlbs  27164  frlmup1  27165  ellspd  27169  imasgim  27179  islinds  27194  islindf2  27199  f1lindf  27207  islindf4  27223  lnr2i  27235  elmnc  27256  rngunsnply  27293  f1otrspeq  27305  pmtrfrn  27315  psgnunilem1  27331  psgnunilem5  27332  psgnunilem2  27333  psgnunilem3  27334  psgneldm2  27342  mat1  27397  issdrg  27420  dvconstbi  27466  stoweidlem27  27690  stoweidlem29  27692  stoweidlem31  27694  stoweidlem34  27697  stoweidlem48  27711  stoweidlem59  27722  afvelrnb  27941  afvelrnb0  27942  ubmelfzo  28038  elfzelfzccat  28079  swrd0swrd  28084  swrdswrd  28086  swrdswrd0  28088  swrdccatin1  28091  swrdccatin2  28093  swrdccatin12lem2  28095  swrdccatin12lem3b  28097  swrdccatin12lem3c  28098  swrdccatin12lem3  28099  swrdccatin12  28101  swrdccatin12b  28102  swrdccat3  28104  swrdccat3b  28106  reumodprminv  28111  2shwrd1lem1  28136  2shwrd1lem2  28137  2shwrd2lem1  28142  2shwrd2lem2  28143  shwrdeqdif2  28156  shwrdeqdif2s  28157  usgra2pthlem1  28184  2wlksot  28208  2spthsot  28209  el2wlkonot  28210  el2spthonot  28211  el2spthonot0  28212  2wlkonot3v  28216  2spthonot3v  28217  el2wlksoton  28219  el2spthsoton  28220  el2wlksotot  28223  usg2spthonot  28229  usg2spthonot0  28230  frgrancvvdeqlem3  28279  usg2spot2nb  28312  usgreg2spot  28314  2spotmdisj  28315  bnj945  28998  bnj1400  29061  bnj18eq1  29152  bnj916  29158  bnj1014  29185  bnj1015  29186  bnj1110  29205  bnj1417  29264  islshp  29616  islsat  29628  lcvfbr  29657  islfl  29697  ellkr  29726  islshpkrN  29757  ldual1dim  29803  isopos  29817  cmtfvalN  29847  cvrfval  29905  isat  29923  islln  30142  islpln  30166  islvol  30209  isline  30375  ispointN  30378  ispsubsp  30381  elpmap  30394  elpmapat  30400  elpadd  30435  paddclN  30478  elpclN  30528  elpcliN  30529  pclfinN  30536  pclcmpatN  30537  ispsubclN  30573  iswatN  30630  islhp  30632  islaut  30719  ispautN  30735  isldil  30746  isltrn  30755  isdilN  30790  istrnN  30793  istendo  31396  dvhb1dimN  31622  erng1lem  31623  erngdvlem4-rN  31635  diaelval  31670  diaeldm  31673  dia1dimid  31700  cdlemm10N  31755  dibopelvalN  31780  dibopelval2  31782  dibelval3  31784  dibelval1st  31786  dibelval2nd  31789  dibeldmN  31795  dibvalrel  31800  dibglbN  31803  dicffval  31811  dicfval  31812  dicopelval  31814  dicelvalN  31815  dicelval3  31817  dicvalrelN  31822  dicelval1sta  31824  diclspsn  31831  dihopelvalbN  31875  dihopelvalcqat  31883  dihopelvalcpre  31885  dihvalrel  31916  dih1  31923  dihmeetlem4preN  31943  dihmeetlem13N  31956  dih1dimatlem  31966  dochnel2  32029  dihjatcclem4  32058  dvh2dim  32082  dvh3dim  32083  dvh4dimN  32084  dochfln0  32114  lpolsetN  32119  islpolN  32120  lcfrvalsnN  32178  lcfrlem21  32200  lcfrlem27  32206  lcfrlem37  32216  lcfr  32222  lcdlss  32256  mapdcv  32297  hdmap1fval  32434  hdmapffval  32466  hdmapfval  32467  hdmapval  32468  hgmapffval  32525  hgmapfval  32526  hdmapellkr  32554  hlhilhillem  32600
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2428  df-clel 2431
  Copyright terms: Public domain W3C validator