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

Theorem eleq2d 2454
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 2448 . 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 1649    e. wcel 1717
This theorem is referenced by:  eleq12d  2455  eleqtrd  2463  neleqtrd  2482  neleqtrrd  2483  abeq2d  2496  nfceqdf  2522  drnfc1  2539  drnfc2  2540  sbcbid  3157  cbvcsb  3198  sbcel1g  3213  csbeq2d  3218  csbie2g  3240  cbvralcsf  3254  cbvreucsf  3256  cbvrabcsf  3257  cbviun  4069  cbviin  4070  iinxsng  4108  iinxprg  4109  iunxsng  4110  cbvdisj  4133  disjor  4137  mpteq12f  4226  axpweq  4317  rabxfrd  4684  0nelelxp  4847  opeliunxp  4869  opeliunxp2  4953  iunxpf  4961  elrelimasn  5168  elimasng  5170  elimasni  5171  ressn  5348  funfni  5485  fnbr  5487  fun11iun  5635  dffv3  5664  fvelrnb  5713  fvun1  5733  fvco2  5737  elpreima  5789  dff3  5821  fmptco  5840  fnpr  5889  fnprOLD  5890  zfrep6  5907  funfvima3  5914  eluniima  5936  dff13  5943  f1eqcocnv  5967  isoini  5997  mpt2eq123dva  6074  cbvmpt2x  6089  ovelrn  6161  elovmpt2  6230  fmpt2x  6356  bropopvvv  6365  mpt2xopn0yelv  6400  mpt2xopovel  6407  isprmpt2  6413  rntpos  6428  riotaeqdv  6486  onoviun  6541  smoel  6558  smoiso  6560  smoel2  6561  smo11  6562  tfrlem9  6582  oalimcl  6739  oaass  6740  omordi  6745  omordlim  6756  omlimcl  6757  odi  6758  omeulem1  6761  omeulem2  6762  oen0  6765  oeordi  6766  oeordsuc  6773  oelimcl  6779  oeeulem  6780  oeeui  6781  nnmordi  6810  oaabs2  6824  omabs  6826  omsmolem  6832  ereldm  6884  iiner  6912  elmapg  6967  elpmg  6968  elixpsn  7037  ixpsnf1o  7038  boxriin  7040  omxpenlem  7145  pw2f1olem  7148  phplem4  7225  php3  7229  elfi  7353  dffi3  7371  marypha2lem2  7376  ordiso2  7417  wemapso2lem  7452  elharval  7464  inf3lemd  7515  inf3lem1  7516  inf3lem2  7517  inf3lem3  7518  cantnfs  7554  cantnfp1lem3  7569  cantnflem1b  7575  cantnflem1  7578  trcl  7597  r1sdom  7633  r1ordg  7637  r1pwss  7643  tz9.12lem3  7648  tz9.12  7649  r1elwf  7655  rankr1ai  7657  rankidb  7659  rankr1bg  7662  rankval2  7677  rankunb  7709  tcrank  7741  fseqdom  7840  acni  7859  acni2  7860  acndom  7865  infpwfien  7876  alephnbtwn  7885  cardaleph  7903  cardinfima  7911  iunfictbso  7928  dfac3  7935  dfac5lem5  7941  dfac5  7942  dfac9  7949  dfac12r  7959  kmlem2  7964  kmlem12  7974  kmlem13  7975  kmlem14  7976  ackbij2lem3  8054  ackbij2  8056  cofsmo  8082  cfsmolem  8083  alephsing  8089  fin23lem30  8155  isf32lem9  8174  itunisuc  8232  axcc2lem  8249  axcc3  8251  domtriomlem  8255  axdc2lem  8261  axdc2  8262  axdc3lem2  8264  axdc3lem4  8266  axdc4lem  8268  ac6c4  8294  zorn2lem1  8309  ttukeylem6  8327  pwcfsdom  8391  axregndlem2  8411  axinfndlem1  8413  axacndlem4  8418  axacnd  8420  pwfseqlem1  8466  inar1  8583  inatsk  8586  gruurn  8606  grur1  8628  grothpw  8634  eltskm  8651  genpelv  8810  eluz1  10424  eluzadd  10446  eluzsub  10447  elixx1  10857  elixx3g  10861  elioo2  10889  elfz1  10980  elfz2  10982  elfzp1  11029  fzpr  11033  fzsuc2  11035  fzrev3  11042  elfzp12  11056  elfzo  11072  elfzom1b  11118  fzosplitsni  11123  seqp1  11265  seqf1o  11291  bcval  11522  bcpasc  11539  hashf1lem1  11631  ccatfval  11669  ccatlid  11675  ccatass  11677  swrdid  11699  ccatswrd  11700  swrdccat2  11702  cats1un  11717  revccat  11725  revrev  11726  revco  11730  ccatco  11731  shftfn  11815  shftval  11816  limsupgle  12198  ello12  12237  elo12  12248  isercolllem3  12387  sumeq1f  12409  fsumsplit  12460  sumsplit  12479  fsum2dlem  12481  fsumcom2  12485  fsumparts  12512  explecnv  12571  eftlub  12637  divalgmod  12853  bitsval  12863  bitsp1e  12871  bitsp1o  12872  sadfval  12891  sadcp1  12894  sadval  12895  sadcadd  12897  sadadd2  12899  saddisjlem  12903  sadadd  12906  sadass  12910  smufval  12916  smuval  12920  smuval2  12921  smupvallem  12922  smu01lem  12924  smueqlem  12929  smumul  12932  bezoutlem2  12966  bezoutlem4  12968  algfx  12998  eucalgcvga  13004  unbenlem  13203  prmreclem5  13215  vdwapval  13268  vdwapun  13269  vdwnnlem1  13290  vdwnn  13293  ramval  13303  0ram  13315  ramub1lem2  13322  prmlem0  13355  elrest  13582  prdsbasmpt  13619  prdsleval  13626  prdsbasmpt2  13631  pwselbasb  13637  imasaddfnlem  13680  imasvscafn  13689  divsfval  13699  ismre  13742  mreunirn  13753  mrisval  13782  ismri  13783  isacs  13803  catidd  13832  iscatd2  13833  ismon  13886  isepi  13893  sectffval  13903  sectfval  13904  issubc  13962  isfunc  13988  funcres  14020  funcpropd  14024  ffthiso  14053  isnat  14071  isnat2  14072  fuciso  14099  arwhoma  14127  elsetchom  14163  setcmon  14169  setcepi  14170  setciso  14173  catciso  14189  hofcl  14283  hofpropd  14291  yonedalem4c  14301  yonedainv  14305  yonffthlem  14306  poslubdg  14502  acsficl2d  14529  acsmapd  14531  psref  14567  psss  14573  dirge  14609  grpidval  14634  grpidd  14645  ismndd  14646  mndpropd  14648  grpidpropd  14649  imasmnd2  14659  imasmnd  14660  ismhm  14667  issubm  14675  gsumccat  14714  imasgrp2  14860  imasgrp  14861  issubg  14871  subginv  14878  isnsg  14896  isghm  14933  resghm2b  14951  conjnmzb  14967  conjnsg  14968  ghmpropd  14970  isga  14995  elcntz  15048  elcntzsn  15051  cntzrcl  15053  resscntz  15057  gexdvds  15145  gex1  15152  isslw  15169  sylow3lem2  15189  lsmelvalx  15201  pj1ghm  15262  efgtlen  15285  efgs1b  15295  efgsfo  15298  efgredlemc  15304  frgp0  15319  frgpmhm  15324  divsabl  15407  frgpnabllem1  15411  0cyg  15429  cycsubgcyg  15437  gsumval3  15441  gsumcllem  15443  gsumzaddlem  15453  gsumzsplit  15456  eldprd  15489  dprdcntz2  15523  dprd2d2  15529  dmdprdsplit2lem  15530  dmdprdsplit2  15531  dprdsplit  15533  ablfac2  15574  isrngd  15625  imasrng  15652  dvdsrval  15677  isunit  15689  dvdsrpropd  15728  isirred  15731  isrhm  15751  drngunit  15767  isdrngd  15787  issubrg  15795  opprsubrg  15816  rhmpropd  15830  isabv  15834  issrngd  15876  islmod  15881  lmodprop2d  15933  islss  15938  islssd  15939  lssats2  16003  lspsnel  16006  islmhm  16030  lmhmf1o  16049  lmhmima  16050  lmhmpreima  16051  reslmhm  16055  lmhmpropd  16072  islbs  16075  lspprel  16093  lspfixed  16127  lbsacsbs  16155  lbsextlem1  16157  lbsextlem2  16158  lbsextlem3  16159  lbsextlem4  16160  lidlmcl  16215  divscrng  16238  islpidl  16244  lidldvgen  16253  mplsubglem  16425  mpllsslem  16426  mplmonmul  16454  mplrcl  16477  subrgascl  16485  subrgasclcl  16486  strov2rcl  16558  zrhrhmb  16715  znf1o  16755  frgpcyg  16777  isphld  16808  elocv  16818  iscss  16833  isobs  16870  obs2ss  16879  istopon  16913  eltg  16945  eltg2  16946  eltop  16962  eltop2  16963  eltop3  16964  pptbas  16995  iscld  17014  neiss2  17088  isnei  17090  neiptopnei  17119  neiptopreu  17120  lpfval  17125  lpval  17126  islp  17127  maxlp  17133  islpi  17135  neitr  17166  restlp  17169  ordtbas2  17177  ordtrest2  17190  lmfval  17218  cnfval  17219  iscn  17221  iscnp  17223  tgcn  17238  tgcnp  17239  lmbrf  17246  cnpresti  17274  ist1  17307  ist1-2  17333  cnt1  17336  haust1  17338  cmpfi  17393  cmpfii  17394  1stcfb  17429  2ndc1stc  17435  1stcrest  17437  2ndcdisj  17440  1stcelcls  17445  nllyi  17459  subislly  17465  kgenval  17488  elkgen  17489  kgencn2  17510  txbas  17520  eltx  17521  ptval  17523  ptpjpre1  17524  ptopn2  17537  ptpjopn  17565  ptclsg  17568  xkoccn  17572  txdis  17585  txdis1cn  17588  ptrescn  17592  hausdiag  17598  hauseqlcld  17599  txhaus  17600  xkohaus  17606  elqtop  17650  qtopeu  17669  kqcldsat  17686  hmeofval  17711  ptuncnv  17760  ptunhmeo  17761  elmptrab  17780  fbdmn0  17787  elfg  17824  elfilss  17829  filunirn  17835  fixufil  17875  elfm  17900  rnelfmlem  17905  rnelfm  17906  fmfnfmlem4  17910  elflim2  17917  flimtopon  17923  elflim  17924  hausflim  17934  flimcls  17938  flfnei  17944  isflf  17946  hausflf  17950  cnpflf  17954  cnflf  17955  txflf  17959  isfcls  17962  fclstopon  17965  isfcls2  17966  fclssscls  17971  fclsnei  17972  fclsfnflim  17980  flimfnfcls  17981  isfcf  17987  fcfelbas  17989  cnpfcf  17994  cnfcf  17995  alexsublem  17996  alexsubALTlem3  18001  cnextfun  18016  cnextfvval  18017  cnextf  18018  cnextcn  18019  tmdgsum2  18047  tgpconcomp  18063  ghmcnp  18065  divstgplem  18071  eltsms  18083  haustsms  18086  tsmsgsum  18089  tsmssubm  18093  tsmssplit  18102  isust  18154  elrnust  18175  ustbas  18178  elutop  18184  ustuqtoplem  18190  ustuqtop4  18195  ustuqtop  18197  utopsnneiplem  18198  utopsnneip  18199  utopsnnei  18200  isusp  18212  isucn  18229  ucncn  18236  iscfilu  18239  neipcfilu  18247  iscusp  18250  cnextucn  18254  ismet  18262  isxmet  18263  elbl  18323  elmopn  18362  prdsbl  18411  neibl  18421  met1stc  18441  metrest  18444  prdsxmslem2  18449  txmetcnp  18467  txmetcn  18468  metuval  18469  metustsym  18475  cfilucfil2  18481  elbl4  18483  metuel  18484  metutop  18487  restmetu  18489  metucn  18490  tngngp  18566  isnmhm  18651  zcld  18715  metnrmlem1a  18759  elcncf  18790  cncfcnvcn  18822  cnheibor  18851  lebnumlem1  18857  ishtpy  18868  isphtpy  18877  om1elbas  18928  elpi1  18941  pi1xfr  18951  pi1coghm  18957  tchcph  19065  lmmbrf  19086  iscfil  19089  iscau  19100  iscauf  19104  caucfil  19107  iscmet  19108  cmetcaulem  19112  iscmet3lem1  19115  iscmet3lem2  19116  iscmet3  19117  bcthlem1  19146  cmsss  19172  cmetcusp1  19174  cmetcusp  19175  minveclem3b  19196  ovolfioo  19231  ovolficc  19232  ovolctb  19253  ovoliunnul  19270  ovolshftlem1  19272  sca2rab  19275  ovolscalem1  19276  ovolicc2lem1  19280  ovolicc2lem2  19281  ovolicc2lem4  19283  ovolicc2lem5  19284  iundisj  19309  iunmbl2  19318  uniioombllem3  19344  vitalilem2  19368  vitalilem3  19369  mbfss  19405  i1faddlem  19452  i1fmullem  19453  mbfi1fseqlem2  19475  mbfi1fseqlem4  19477  mbfi1fseq  19480  itg2splitlem  19507  itg2split  19508  itg2monolem1  19509  itg2gt0  19519  isibl  19524  iblss2  19564  itgss3  19573  itgsplit  19594  ellimc  19627  limcmo  19636  cnlimc  19642  limciun  19648  limcun  19649  eldv  19652  dvbsss  19656  dvreslem  19663  elcpn  19687  dvaddf  19695  dvmulf  19696  dvcof  19701  rolle  19741  dvlip2  19746  dvivthlem1  19759  lhop1  19765  lhop2  19766  ftc1cn  19794  mpfind  19832  fta1glem2  19956  plyco0  19978  elply  19981  ply1termlem  19989  eltayl  20143  tayl0  20145  taylplem1  20146  taylplem2  20147  dvtaylp  20153  taylthlem1  20156  taylthlem2  20157  abelth  20224  cxpcn3  20499  rlimcnp  20671  fsumharmonic  20717  dchrelbas  20887  pntrsumbnd2  21128  ostth2lem2  21195  usgra2edg1  21269  usgraidx2vlem1  21276  usgraidx2vlem2  21277  nbgraop  21302  nbgrael  21304  nbusgra  21306  nbgraeledg  21308  nbgraf1olem1  21317  nbgraf1olem3  21319  nbgraf1olem5  21321  nbgraf1o  21323  iscusgra  21331  sizeusglecusglem1  21359  isuvtx  21363  uvtxel  21364  uvtxisvtx  21365  wlks  21390  iswlk  21391  istrl  21401  ispth  21422  isspth  21423  fargshiftlem  21469  fargshiftfv  21470  fargshiftfo  21473  vdgrfval  21514  vdgrun  21520  vdgrfiun  21521  vdgr1a  21525  eupap1  21546  eupath2lem3  21549  ex-res  21597  isabloda  21735  issubgo  21739  isass  21752  elghomlem2  21798  ghablo  21805  iscom2  21848  rngoidmlem  21859  rngo1cl  21865  isssp  22071  sspn  22083  islno  22102  isblo  22131  nmlno0  22144  ishmo  22160  dipdir  22191  dipass  22194  ubthlem1  22220  ubthlem2  22221  htthlem  22268  htth  22269  ocel  22631  ocnel  22648  shsel  22664  shsel2  22672  shmodsi  22739  pjhtheu  22744  pjeq  22749  axpjpj  22770  pjoc2  22789  elspani  22893  h1de2ctlem  22905  elspansn  22916  elspansn2  22917  elnlfn  23279  eleigvec  23308  riesz3i  23413  iuneq12daf  23851  iuneq12df  23852  iunrdx  23858  cbvdisjf  23859  disjorf  23865  disjabrex  23868  disjabrexf  23869  iundisjf  23872  disjrdx  23874  elunirn2  23905  abfmpunirn  23906  abfmpeld  23908  abfmpel  23909  fmptdF  23911  fmptcof2  23918  funcnvmptOLD  23923  funcnvmpt  23924  xrofsup  23962  iundisjfi  23990  eliccioo  24016  xrge0tsmsbi  24053  cnre2csqima  24113  fmcncfil  24121  ofcfval  24277  measvuni  24362  meascnbl  24367  faeval  24391  ismbfm  24396  elunirnmbfm  24397  isanmbfm  24400  imambfm  24406  itgeq12dv  24435  rrvmbfm  24479  elorvc  24496  elorrvc  24500  dstfrvunirn  24511  ballotlemfc0  24529  ballotlemfcc  24530  ballotlemsima  24552  ballotlemrv  24556  subfacp1lem2b  24646  subfacp1lem4  24648  subfacp1lem5  24649  subfacp1lem6  24650  ptpcon  24699  cvmscbv  24724  iscvm  24725  cvmsi  24731  cvmsval  24732  cvmliftmolem1  24747  cvmlift2lem12  24780  cvmlift2lem13  24781  cvmlift3lem7  24791  snmlval  24797  elgiso  24886  fprodser  25054  fprodsplit  25068  mpteq12d  25152  predbrg  25210  trpredrec  25265  wfrlem9  25288  wfrlem12  25291  fvnobday  25360  nodenselem3  25361  nodenselem5  25363  nofulllem5  25384  elee  25547  brbtwn  25552  brcgr  25553  axlowdimlem16  25610  funtransport  25679  fvtransport  25680  brcolinear  25707  colineardim1  25709  funray  25788  fvray  25789  funline  25790  fvline  25792  lineelsb2  25796  rankelg  25823  rankeq1o  25826  elhf2  25830  0hf  25832  volsupnfl  25956  itg2addnclem  25957  itg2gt0cn  25960  islocfin  26067  lfinpfin  26074  locfindis  26076  locfincf  26077  comppfsc  26078  neibastop2lem  26080  neibastop3  26082  eltail  26094  indexdom  26127  incsequz  26143  istotbnd  26169  istotbnd3  26171  0totbnd  26173  sstotbnd  26175  sstotbnd3  26176  isbnd  26180  prdstotbnd  26194  cntotbnd  26196  isismty  26201  heibor1lem  26209  heiborlem2  26212  heiborlem3  26213  heibor  26221  exidcl  26242  exidreslem  26243  divrngcl  26264  isdrngo2  26265  isrngohom  26272  isrngoiso  26285  isriscg  26291  iscringd  26300  isidl  26315  ispridl  26335  ismaxidl  26341  prter3  26422  fnelfp  26427  fnelnfp  26429  isnacs  26449  mrefg2  26452  elmzpcl  26474  mzpcompact2  26500  eldiophb  26506  elpell1qr  26601  elpell14qr  26603  elpell1234qr  26605  pw2f1ocnv  26799  pw2f1o2val2  26802  aomclem4  26823  aomclem6  26825  islssfg2  26838  pwssplit3  26859  dsmmbas2  26872  dsmmfi  26873  dsmmelbas  26874  dsmmlss  26879  frlmelbas  26893  frlmlbs  26918  frlmup1  26919  ellspd  26923  imasgim  26933  islinds  26948  islindf2  26953  f1lindf  26961  islindf4  26977  lnr2i  26989  elmnc  27010  rngunsnply  27047  f1otrspeq  27059  pmtrfrn  27069  psgnunilem1  27085  psgnunilem5  27086  psgnunilem2  27087  psgnunilem3  27088  psgneldm2  27096  mat1  27151  issdrg  27174  dvconstbi  27220  stoweidlem27  27444  stoweidlem29  27446  stoweidlem31  27448  stoweidlem34  27451  stoweidlem48  27465  stoweidlem59  27476  afvelrnb  27696  afvelrnb0  27697  frgrancvvdeqlem3  27784  bnj945  28482  bnj1400  28545  bnj18eq1  28636  bnj916  28642  bnj1014  28669  bnj1015  28670  bnj1110  28689  bnj1417  28748  islshp  29094  islsat  29106  lcvfbr  29135  islfl  29175  ellkr  29204  islshpkrN  29235  ldual1dim  29281  isopos  29295  cmtfvalN  29325  cvrfval  29383  isat  29401  islln  29620  islpln  29644  islvol  29687  isline  29853  ispointN  29856  ispsubsp  29859  elpmap  29872  elpmapat  29878  elpadd  29913  paddclN  29956  elpclN  30006  elpcliN  30007  pclfinN  30014  pclcmpatN  30015  ispsubclN  30051  iswatN  30108  islhp  30110  islaut  30197  ispautN  30213  isldil  30224  isltrn  30233  isdilN  30268  istrnN  30271  istendo  30874  dvhb1dimN  31100  erng1lem  31101  erngdvlem4-rN  31113  diaelval  31148  diaeldm  31151  dia1dimid  31178  cdlemm10N  31233  dibopelvalN  31258  dibopelval2  31260  dibelval3  31262  dibelval1st  31264  dibelval2nd  31267  dibeldmN  31273  dibvalrel  31278  dibglbN  31281  dicffval  31289  dicfval  31290  dicopelval  31292  dicelvalN  31293  dicelval3  31295  dicvalrelN  31300  dicelval1sta  31302  diclspsn  31309  dihopelvalbN  31353  dihopelvalcqat  31361  dihopelvalcpre  31363  dihvalrel  31394  dih1  31401  dihmeetlem4preN  31421  dihmeetlem13N  31434  dih1dimatlem  31444  dochnel2  31507  dihjatcclem4  31536  dvh2dim  31560  dvh3dim  31561  dvh4dimN  31562  dochfln0  31592  lpolsetN  31597  islpolN  31598  lcfrvalsnN  31656  lcfrlem21  31678  lcfrlem27  31684  lcfrlem37  31694  lcfr  31700  lcdlss  31734  mapdcv  31775  hdmap1fval  31912  hdmapffval  31944  hdmapfval  31945  hdmapval  31946  hgmapffval  32003  hgmapfval  32004  hdmapellkr  32032  hlhilhillem  32078
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2380  df-clel 2383
  Copyright terms: Public domain W3C validator