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

Theorem eleq2d 2363
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 2357 . 2  |-  ( A  =  B  ->  ( C  e.  A  <->  C  e.  B ) )
31, 2syl 15 1  |-  ( ph  ->  ( C  e.  A  <->  C  e.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1632    e. wcel 1696
This theorem is referenced by:  eleq12d  2364  eleqtrd  2372  neleqtrd  2391  neleqtrrd  2392  abeq2d  2405  nfceqdf  2431  drnfc1  2448  drnfc2  2449  sbcbid  3057  cbvcsb  3098  sbcel1g  3113  csbeq2d  3118  csbie2g  3140  cbvralcsf  3156  cbvreucsf  3158  cbvrabcsf  3159  cbviun  3955  cbviin  3956  iinxsng  3994  iinxprg  3995  iunxsng  3996  cbvdisj  4019  disjor  4023  mpteq12f  4112  axpweq  4203  rabxfrd  4571  0nelelxp  4734  opeliunxp  4756  opeliunxp2  4840  iunxpf  4848  elrelimasn  5053  elimasng  5055  elimasni  5056  ressn  5227  funfni  5360  fnbr  5362  fun11iun  5509  dffv3  5537  fvelrnb  5586  fvun1  5606  fvco2  5610  elpreima  5661  dff3  5689  fmptco  5707  zfrep6  5764  funfvima3  5771  eluniima  5792  dff13  5799  f1eqcocnv  5821  isoini  5851  mpt2eq123dva  5925  cbvmpt2x  5940  ovelrn  6012  elovmpt2  6080  fmpt2x  6206  rntpos  6263  riotaeqdv  6321  onoviun  6376  smoel  6393  smoiso  6395  smoel2  6396  smo11  6397  smoord  6398  tfrlem9  6417  oalimcl  6574  oaass  6575  omordi  6580  omordlim  6591  omlimcl  6592  odi  6593  omeulem1  6596  omeulem2  6597  omopth2  6598  oen0  6600  oeordi  6601  oeordsuc  6608  oelimcl  6614  oeeulem  6615  oeeui  6616  nnmordi  6645  oaabs2  6659  omabs  6661  omsmolem  6667  ereldm  6719  iiner  6747  elmapg  6801  elpmg  6802  elixpsn  6871  ixpsnf1o  6872  boxriin  6874  omxpenlem  6979  pw2f1olem  6982  phplem4  7059  php3  7063  elfi  7183  dffi3  7200  marypha2lem2  7205  ordiso2  7246  wemapso2lem  7281  elharval  7293  inf3lemd  7344  inf3lem1  7345  inf3lem2  7346  inf3lem3  7347  cantnfs  7383  cantnfp1lem3  7398  cantnflem1b  7404  cantnflem1  7407  trcl  7426  r1sdom  7462  r1ordg  7466  r1pwss  7472  tz9.12lem3  7477  tz9.12  7478  r1elwf  7484  rankr1ai  7486  rankidb  7488  rankr1bg  7491  rankval2  7506  rankunb  7538  tcrank  7570  fseqdom  7669  acni  7688  acni2  7689  acndom  7694  infpwfien  7705  alephnbtwn  7714  cardaleph  7732  cardinfima  7740  iunfictbso  7757  dfac3  7764  dfac5lem5  7770  dfac5  7771  dfac9  7778  dfac12r  7788  kmlem2  7793  kmlem12  7803  kmlem13  7804  kmlem14  7805  ackbij2lem3  7883  ackbij2  7885  cofsmo  7911  cfsmolem  7912  alephsing  7918  fin23lem30  7984  isf32lem9  8003  itunisuc  8061  axcc2lem  8078  axcc3  8080  domtriomlem  8084  axdc2lem  8090  axdc2  8091  axdc3lem2  8093  axdc3lem4  8095  axdc4lem  8097  ac6c4  8124  zorn2lem1  8139  ttukeylem6  8157  pwcfsdom  8221  axregndlem2  8241  axinfndlem1  8243  axacndlem4  8248  axacnd  8250  pwfseqlem1  8296  inar1  8413  inatsk  8416  r1tskina  8420  gruurn  8436  grur1  8458  grothpw  8464  eltskm  8481  genpelv  8640  eluz1  10250  eluzadd  10272  eluzsub  10273  elixx1  10681  elixx3g  10685  elioo2  10713  elfz1  10803  elfz2  10805  elfzp1  10852  fzpr  10856  fzsuc2  10858  fzrev3  10865  elfzp12  10877  elfzo  10893  elfzom1b  10934  fzosplitsni  10937  seqp1  11077  seqf1o  11103  bcval  11333  bcpasc  11349  hashf1lem1  11409  ccatfval  11444  ccatlid  11450  ccatass  11452  swrdid  11474  ccatswrd  11475  swrdccat2  11477  cats1un  11492  revccat  11500  revrev  11501  revco  11505  ccatco  11506  shftfn  11584  shftval  11585  limsupgle  11967  ello12  12006  elo12  12017  isercolllem3  12156  sumeq1f  12177  cbvsum  12184  fsumsplit  12228  sumsplit  12247  fsum2dlem  12249  fsumcom2  12253  fsumparts  12280  explecnv  12339  eftlub  12405  divalgmod  12621  bitsval  12631  bitsp1e  12639  bitsp1o  12640  sadfval  12659  sadcp1  12662  sadval  12663  sadcadd  12665  sadadd2  12667  saddisjlem  12671  sadadd  12674  sadass  12678  smufval  12684  smuval  12688  smuval2  12689  smupvallem  12690  smu01lem  12692  smueqlem  12697  smumul  12700  bezoutlem2  12734  bezoutlem4  12736  algfx  12766  eucalgcvga  12772  unbenlem  12971  prmreclem5  12983  vdwapval  13036  vdwapun  13037  vdwnnlem1  13058  vdwnn  13061  ramval  13071  0ram  13083  ramub1lem2  13090  prmlem0  13123  elrest  13348  prdsbasmpt  13385  prdsleval  13392  prdsbasmpt2  13397  pwselbasb  13403  imasaddfnlem  13446  imasvscafn  13455  divsfval  13465  ismre  13508  mreunirn  13519  mrisval  13548  ismri  13549  isacs  13569  catidd  13598  iscatd2  13599  ismon  13652  isepi  13659  sectffval  13669  sectfval  13670  issubc  13728  isfunc  13754  funcres  13786  funcpropd  13790  ffthiso  13819  isnat  13837  isnat2  13838  fuciso  13865  arwhoma  13893  elsetchom  13929  setcmon  13935  setcepi  13936  setciso  13939  catciso  13955  hofcl  14049  hofpropd  14057  yonedalem4c  14067  yonedainv  14071  yonffthlem  14072  poslubdg  14268  acsficl2d  14295  acsmapd  14297  psref  14333  psss  14339  dirge  14375  grpidval  14400  grpidd  14411  ismndd  14412  mndpropd  14414  grpidpropd  14415  imasmnd2  14425  imasmnd  14426  ismhm  14433  issubm  14441  gsumccat  14480  imasgrp2  14626  imasgrp  14627  issubg  14637  subginv  14644  isnsg  14662  isghm  14699  resghm2b  14717  conjnmzb  14733  conjnsg  14734  ghmpropd  14736  isga  14761  elcntz  14814  elcntzsn  14817  cntzrcl  14819  resscntz  14823  gexdvds  14911  gex1  14918  isslw  14935  sylow3lem2  14955  lsmelvalx  14967  pj1ghm  15028  efgtlen  15051  efgs1b  15061  efgsfo  15064  efgredlemc  15070  frgp0  15085  frgpmhm  15090  divsabl  15173  frgpnabllem1  15177  0cyg  15195  cycsubgcyg  15203  gsumval3  15207  gsumcllem  15209  gsumzaddlem  15219  gsumzsplit  15222  eldprd  15255  dprdcntz2  15289  dprd2d2  15295  dmdprdsplit2lem  15296  dmdprdsplit2  15297  dprdsplit  15299  ablfac2  15340  isrngd  15391  imasrng  15418  dvdsrval  15443  isunit  15455  dvdsrpropd  15494  isirred  15497  isrhm  15517  drngunit  15533  isdrngd  15553  issubrg  15561  opprsubrg  15582  rhmpropd  15596  isabv  15600  issrngd  15642  islmod  15647  lmodprop2d  15703  islss  15708  islssd  15709  lssats2  15773  lspsnel  15776  islmhm  15800  lmhmf1o  15819  lmhmima  15820  lmhmpreima  15821  reslmhm  15825  lmhmpropd  15842  islbs  15845  lspprel  15863  lspfixed  15897  lspindp4  15906  lsppratlem3  15918  lbsacsbs  15925  lbsextlem1  15927  lbsextlem2  15928  lbsextlem3  15929  lbsextlem4  15930  lidlmcl  15985  divscrng  16008  islpidl  16014  lidldvgen  16023  mplsubglem  16195  mpllsslem  16196  mplmonmul  16224  mplrcl  16247  subrgascl  16255  subrgasclcl  16256  strov2rcl  16331  zrhrhmb  16481  znf1o  16521  frgpcyg  16543  isphld  16574  elocv  16584  iscss  16599  isobs  16636  obs2ss  16645  istopon  16679  eltg  16711  eltg2  16712  eltop  16728  eltop2  16729  eltop3  16730  pptbas  16761  iscld  16780  neiss2  16854  isnei  16856  lpfval  16886  lpval  16887  islp  16888  maxlp  16894  islpi  16896  restlp  16929  ordtbas2  16937  ordtrest2  16950  lmfval  16978  cnfval  16979  iscn  16981  iscnp  16983  tgcn  16998  tgcnp  16999  lmbrf  17006  cnpresti  17032  ist1  17065  ist1-2  17091  cnt1  17094  haust1  17096  cmpfi  17151  cmpfii  17152  1stcfb  17187  2ndc1stc  17193  1stcrest  17195  2ndcdisj  17198  1stcelcls  17203  nllyi  17217  subislly  17223  kgenval  17246  elkgen  17247  kgencn2  17268  txbas  17278  eltx  17279  ptval  17281  ptpjpre1  17282  ptopn2  17295  ptpjopn  17322  ptclsg  17325  xkoccn  17329  txdis  17342  txdis1cn  17345  ptrescn  17349  hausdiag  17355  hauseqlcld  17356  txhaus  17357  xkohaus  17363  elqtop  17404  qtopeu  17423  kqcldsat  17440  hmeofval  17465  ptuncnv  17514  ptunhmeo  17515  elmptrab  17538  fbdmn0  17545  elfg  17582  elfilss  17587  filunirn  17593  fixufil  17633  elfm  17658  rnelfmlem  17663  rnelfm  17664  fmfnfmlem4  17668  elflim2  17675  flimtopon  17681  elflim  17682  hausflim  17692  flimcls  17696  flfnei  17702  isflf  17704  hausflf  17708  cnpflf  17712  cnflf  17713  txflf  17717  isfcls  17720  fclstopon  17723  isfcls2  17724  fclssscls  17729  fclsnei  17730  fclsfnflim  17738  flimfnfcls  17739  isfcf  17745  fcfelbas  17747  cnpfcf  17752  cnfcf  17753  alexsublem  17754  alexsubALTlem3  17759  tmdgsum2  17795  tgpconcomp  17811  ghmcnp  17813  divstgplem  17819  eltsms  17831  haustsms  17834  tsmsgsum  17837  tsmssubm  17841  tsmssplit  17850  ismet  17904  isxmet  17905  elbl  17965  elmopn  18004  prdsbl  18053  neibl  18063  met1stc  18083  metrest  18086  prdsxmslem2  18091  txmetcnp  18109  txmetcn  18110  tngngp  18186  isnmhm  18271  zcld  18335  metnrmlem1a  18378  elcncf  18409  cncfcnvcn  18440  cnheibor  18469  lebnumlem1  18475  ishtpy  18486  isphtpy  18495  om1elbas  18546  elpi1  18559  pi1xfr  18569  pi1coghm  18575  tchcph  18683  lmmbrf  18704  iscfil  18707  iscau  18718  iscauf  18722  caucfil  18725  iscmet  18726  cmetcaulem  18730  iscmet3lem1  18733  iscmet3lem2  18734  iscmet3  18735  bcthlem1  18762  cmsss  18788  minveclem3b  18808  ovolfioo  18843  ovolficc  18844  ovolctb  18865  ovoliunnul  18882  ovolshftlem1  18884  sca2rab  18887  ovolscalem1  18888  ovolicc2lem1  18892  ovolicc2lem2  18893  ovolicc2lem4  18895  ovolicc2lem5  18896  iundisj  18921  iunmbl2  18930  uniioombllem3  18956  vitalilem2  18980  vitalilem3  18981  mbfss  19017  i1faddlem  19064  i1fmullem  19065  mbfi1fseqlem2  19087  mbfi1fseqlem4  19089  mbfi1fseq  19092  itg2splitlem  19119  itg2split  19120  itg2monolem1  19121  itg2gt0  19131  isibl  19136  iblss2  19176  itgss3  19185  itgsplit  19206  ellimc  19239  limcmo  19248  cnlimc  19254  limciun  19260  limcun  19261  eldv  19264  dvbsss  19268  dvreslem  19275  elcpn  19299  dvaddf  19307  dvmulf  19308  dvcof  19313  rolle  19353  dvlip2  19358  dvivthlem1  19371  lhop1  19377  lhop2  19378  ftc1cn  19406  mpfind  19444  fta1glem2  19568  plyco0  19590  elply  19593  ply1termlem  19601  eltayl  19755  tayl0  19757  taylplem1  19758  taylplem2  19759  dvtaylp  19765  taylthlem1  19768  taylthlem2  19769  abelth  19833  cxpcn3  20104  rlimcnp  20276  fsumharmonic  20321  dchrelbas  20491  pntrsumbnd2  20732  ostth2lem2  20799  ex-res  20844  isabloda  20982  issubgo  20986  isass  20999  elghomlem2  21045  ghablo  21052  iscom2  21095  rngoidmlem  21106  rngo1cl  21112  isssp  21316  sspn  21328  islno  21347  isblo  21376  nmlno0  21389  ishmo  21405  dipdir  21436  dipass  21439  ubthlem1  21465  ubthlem2  21466  htthlem  21513  htth  21514  ocel  21876  ocnel  21893  shsel  21909  shsel2  21917  shmodsi  21984  pjhtheu  21989  pjeq  21994  axpjpj  22015  pjoc2  22034  elspani  22138  h1de2ctlem  22150  elspansn  22161  elspansn2  22162  elnlfn  22524  eleigvec  22553  riesz3i  22658  ballotlemfc0  23067  ballotlemfcc  23068  ballotlemsima  23090  ballotlemrv  23094  eliccioo  23131  iuneq12daf  23170  iuneq12df  23171  iunrdx  23177  itgeq12dv  23211  elunirn2  23230  fmptdF  23236  fmptcof2  23244  funcnvmptOLD  23249  funcnvmpt  23250  xrofsup  23270  cnre2csqima  23310  cbvdisjf  23365  disjorf  23371  disjabrex  23374  disjabrexf  23375  iundisjfi  23378  iundisjf  23380  disjrdx  23385  xrge0tsmsbi  23398  ofcfval  23474  measvuni  23557  measiuns  23559  meascnbl  23561  ismbfm  23572  elunirnmbfm  23573  isanmbfm  23576  imambfm  23582  dya2iocrrnval  23597  probfinmeasb  23647  rrvmbfm  23660  elorvc  23675  elorrvc  23679  dstrvprob  23687  dstfrvel  23689  dstfrvunirn  23690  subfacp1lem2b  23727  subfacp1lem4  23729  subfacp1lem5  23730  subfacp1lem6  23731  ptpcon  23779  cvmscbv  23804  iscvm  23805  cvmsi  23811  cvmsval  23812  cvmliftmolem1  23827  cvmlift2lem12  23860  cvmlift2lem13  23861  cvmlift3lem7  23871  vdgrfval  23904  vdgrun  23908  vdgr1a  23912  eupap1  23915  eupath2lem3  23918  snmlval  23929  elgiso  24018  mpteq12d  24199  predbrg  24257  trpredrec  24312  wfrlem9  24335  wfrlem12  24338  fvnobday  24407  nodenselem3  24408  nodenselem5  24410  nofulllem5  24431  elee  24594  brbtwn  24599  brcgr  24600  axlowdimlem16  24657  funtransport  24726  fvtransport  24727  brcolinear  24754  colineardim1  24756  funray  24835  fvray  24836  funline  24837  fvline  24839  lineelsb2  24843  rankelg  24870  rankeq1o  24873  elhf2  24877  0hf  24879  itg2addnclem  25003  itg2gt0cn  25006  domrngref  25163  repfuntw  25263  repcpwti  25264  dstr  25274  iscst3  25279  islatalg  25286  valcurfn1  25307  isorhom  25314  isoriso2  25316  puub2  25361  puub  25362  mxlelt  25367  ismxl2  25370  ismnl2  25371  isdir2  25395  prodeq2  25410  prodeq3ii  25411  dffprod  25422  iscom  25436  clfsebsr  25452  imtr  25501  prsubrtr  25502  isfldOLD  25529  idlvalNEW  25548  isidlNEW  25549  basexre  25625  nsn  25633  intopcoaconb  25643  usptoplem  25649  istopx  25650  usptop  25653  prcnt  25654  filint2  25656  conttnf2  25665  limptlimpr2lem1  25677  limptlimpr2lem2  25678  altretop  25703  iintlem1  25713  supnuf  25732  cnegvex2b  25765  rnegvex2b  25766  isded  25839  dedi  25840  iscatOLD  25857  cati  25858  dualded  25886  dualcat2  25887  ishomc  25892  ishomd  25893  ismonb  25913  imonclem  25916  isepib  25923  iepiclem  25926  isfuna  25937  isfunb  25938  issubcata  25949  idsubfun  25961  isinob  25965  issrc  25970  propsrc  25971  isntr  25976  islimcat  25979  vtarsuelt  25998  prismorcset  26017  prismorcset2  26021  domcatfun  26028  codcatfun  26037  prismorcset3  26041  isrocatset  26060  cmppar3  26077  setiscat  26082  isnword  26089  1iskle  26092  indcls2  26099  empklst  26112  clscnc  26113  phckle  26130  psckle  26131  fnckle  26148  cndpv  26152  pgapspf  26155  pgapspf2  26156  lineval22  26185  lineval2a  26188  lineval2b  26189  lineval5a  26191  lineval6a  26192  iscol2  26196  isconcl2b  26201  isibg2  26213  isibg2aa  26215  isibg2aalem1  26216  isibg2aalem2  26217  sgplpte21  26235  sgplpte22  26241  sgplpte21d1  26242  sgplpte21d2  26243  lppotoslem  26246  isray2  26256  isray  26257  isside0  26267  abhp  26276  abhp1  26277  isibcg  26294  islocfin  26399  lfinpfin  26406  locfindis  26408  locfincf  26409  comppfsc  26410  neibastop2lem  26412  neibastop3  26414  eltail  26426  indexdom  26516  incsequz  26561  istotbnd  26596  istotbnd3  26598  0totbnd  26600  sstotbnd  26602  sstotbnd3  26603  isbnd  26607  prdstotbnd  26621  cntotbnd  26623  isismty  26628  heibor1lem  26636  heiborlem2  26639  heiborlem3  26640  heibor  26648  exidcl  26669  exidreslem  26670  divrngcl  26691  isdrngo2  26692  isrngohom  26699  isrngoiso  26712  isriscg  26718  iscringd  26727  isidl  26742  ispridl  26762  ismaxidl  26768  prter3  26853  fnelfp  26858  fnelnfp  26860  isnacs  26882  mrefg2  26885  elmzpcl  26907  mzpcompact2  26933  eldiophb  26939  elpell1qr  27035  elpell14qr  27037  elpell1234qr  27039  pw2f1ocnv  27233  pw2f1o2val2  27236  aomclem4  27257  aomclem6  27259  islssfg2  27272  pwssplit3  27293  dsmmbas2  27306  dsmmfi  27307  dsmmelbas  27308  dsmmlss  27313  frlmelbas  27327  frlmlbs  27352  frlmup1  27353  ellspd  27357  imasgim  27367  islinds  27382  islindf2  27387  f1lindf  27395  islindf4  27411  lnr2i  27423  elmnc  27444  rngunsnply  27481  f1otrspeq  27493  pmtrfrn  27503  psgnunilem1  27519  psgnunilem5  27520  psgnunilem2  27521  psgnunilem3  27522  psgneldm2  27530  mat1  27585  issdrg  27608  dvconstbi  27654  fnchoice  27803  rfcnpre3  27807  rfcnpre4  27808  fmul01lt1lem2  27818  stoweidlem11  27863  stoweidlem26  27878  stoweidlem27  27879  stoweidlem29  27881  stoweidlem31  27883  stoweidlem34  27886  stoweidlem48  27900  stoweidlem57  27909  stoweidlem59  27911  afvelrnb  28131  afvelrnb0  28132  mpt2xopn0yelv  28195  mpt2xopovel  28202  isprmpt2  28208  nbgraop  28274  nbgrael  28275  nbusgra  28277  nbgraeledg  28279  iscusgra  28292  isuvtx  28301  uvtxel  28302  uvtxisvtx  28303  wlks  28328  iswlk  28329  istrl  28336  trlonprop  28341  ispth  28354  isspth  28355  fargshiftlem  28379  fargshiftfv  28380  fargshiftfo  28383  bnj945  29121  bnj1400  29184  bnj18eq1  29275  bnj916  29281  bnj1014  29308  bnj1015  29309  bnj1110  29328  bnj1417  29387  islshp  29791  islsat  29803  lcvfbr  29832  islfl  29872  ellkr  29901  islshpkrN  29932  ldual1dim  29978  isopos  29992  cmtfvalN  30022  cvrfval  30080  isat  30098  islln  30317  islpln  30341  islvol  30384  isline  30550  ispointN  30553  ispsubsp  30556  elpmap  30569  elpmapat  30575  elpadd  30610  paddclN  30653  elpclN  30703  elpcliN  30704  pclfinN  30711  pclcmpatN  30712  ispsubclN  30748  iswatN  30805  islhp  30807  islaut  30894  ispautN  30910  isldil  30921  isltrn  30930  isdilN  30965  istrnN  30968  istendo  31571  dvhb1dimN  31797  erng1lem  31798  erngdvlem4-rN  31810  diaelval  31845  diaeldm  31848  dia1dimid  31875  cdlemm10N  31930  dibopelvalN  31955  dibopelval2  31957  dibelval3  31959  dibelval1st  31961  dibelval2nd  31964  dibeldmN  31970  dibvalrel  31975  dibglbN  31978  dicffval  31986  dicfval  31987  dicopelval  31989  dicelvalN  31990  dicelval3  31992  dicvalrelN  31997  dicelval1sta  31999  diclspsn  32006  dihopelvalbN  32050  dihopelvalcqat  32058  dihopelvalcpre  32060  dihvalrel  32091  dih1  32098  dihmeetlem4preN  32118  dihmeetlem13N  32131  dih1dimatlem  32141  dochnel2  32204  dochnel  32205  dihjatcclem4  32233  dvh2dim  32257  dvh3dim  32258  dvh4dimN  32259  dochfln0  32289  lpolsetN  32294  islpolN  32295  lcfrvalsnN  32353  lcfrlem21  32375  lcfrlem27  32381  lcfrlem37  32391  lcfr  32397  lcdlss  32431  mapdcv  32472  mapdindp2  32533  mapdindp4  32535  mapdh6dN  32551  hdmap1fval  32609  hdmap1l6d  32626  hdmapffval  32641  hdmapfval  32642  hdmapval  32643  hgmapffval  32700  hgmapfval  32701  hdmapellkr  32729  hlhilhillem  32775
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-cleq 2289  df-clel 2292
  Copyright terms: Public domain W3C validator