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

Theorem eleq2d 2471
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 2465 . 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 1721
This theorem is referenced by:  eleq12d  2472  eleqtrd  2480  neleqtrd  2499  neleqtrrd  2500  abeq2d  2513  nfceqdf  2539  drnfc1  2556  drnfc2  2557  sbcbid  3174  cbvcsb  3215  sbcel1g  3230  csbeq2d  3235  csbie2g  3257  cbvralcsf  3271  cbvreucsf  3273  cbvrabcsf  3274  cbviun  4088  cbviin  4089  iinxsng  4127  iinxprg  4128  iunxsng  4129  cbvdisj  4152  disjor  4156  mpteq12f  4245  axpweq  4336  rabxfrd  4703  0nelelxp  4866  opeliunxp  4888  opeliunxp2  4972  iunxpf  4980  elrelimasn  5187  elimasng  5189  elimasni  5190  ressn  5367  funfni  5504  fnbr  5506  fun11iun  5654  dffv3  5683  fvelrnb  5733  fvun1  5753  fvco2  5757  elpreima  5809  dff3  5841  fmptco  5860  fnpr  5909  fnprOLD  5910  zfrep6  5927  funfvima3  5934  eluniima  5956  dff13  5963  f1eqcocnv  5987  isoini  6017  mpt2eq123dva  6094  cbvmpt2x  6109  ovelrn  6181  elovmpt2  6250  fmpt2x  6376  bropopvvv  6385  mpt2xopn0yelv  6423  mpt2xopovel  6430  isprmpt2  6436  rntpos  6451  riotaeqdv  6509  onoviun  6564  smoel  6581  smoiso  6583  smoel2  6584  smo11  6585  tfrlem9  6605  oalimcl  6762  oaass  6763  omordi  6768  omordlim  6779  omlimcl  6780  odi  6781  omeulem1  6784  omeulem2  6785  oen0  6788  oeordi  6789  oeordsuc  6796  oelimcl  6802  oeeulem  6803  oeeui  6804  nnmordi  6833  oaabs2  6847  omabs  6849  omsmolem  6855  ereldm  6907  iiner  6935  elmapg  6990  elpmg  6991  elixpsn  7060  ixpsnf1o  7061  boxriin  7063  omxpenlem  7168  pw2f1olem  7171  phplem4  7248  php3  7252  elfi  7376  dffi3  7394  marypha2lem2  7399  ordiso2  7440  wemapso2lem  7475  elharval  7487  inf3lemd  7538  inf3lem1  7539  inf3lem2  7540  inf3lem3  7541  cantnfs  7577  cantnfp1lem3  7592  cantnflem1b  7598  cantnflem1  7601  trcl  7620  r1sdom  7656  r1ordg  7660  r1pwss  7666  tz9.12lem3  7671  tz9.12  7672  r1elwf  7678  rankr1ai  7680  rankidb  7682  rankr1bg  7685  rankval2  7700  rankunb  7732  tcrank  7764  fseqdom  7863  acni  7882  acni2  7883  acndom  7888  infpwfien  7899  alephnbtwn  7908  cardaleph  7926  cardinfima  7934  iunfictbso  7951  dfac3  7958  dfac5lem5  7964  dfac5  7965  dfac9  7972  dfac12r  7982  kmlem2  7987  kmlem12  7997  kmlem13  7998  kmlem14  7999  ackbij2lem3  8077  ackbij2  8079  cofsmo  8105  cfsmolem  8106  alephsing  8112  fin23lem30  8178  isf32lem9  8197  itunisuc  8255  axcc2lem  8272  axcc3  8274  domtriomlem  8278  axdc2lem  8284  axdc2  8285  axdc3lem2  8287  axdc3lem4  8289  axdc4lem  8291  ac6c4  8317  zorn2lem1  8332  ttukeylem6  8350  pwcfsdom  8414  axregndlem2  8434  axinfndlem1  8436  axacndlem4  8441  axacnd  8443  pwfseqlem1  8489  inar1  8606  inatsk  8609  gruurn  8629  grur1  8651  grothpw  8657  eltskm  8674  genpelv  8833  eluz1  10448  eluzadd  10470  eluzsub  10471  elixx1  10881  elixx3g  10885  elioo2  10913  elfz1  11004  elfz2  11006  elfzp1  11053  fzpr  11057  fzsuc2  11060  fzrev3  11067  elfzp12  11081  elfzo  11097  elfzom1b  11146  fzosplitsni  11151  seqp1  11293  seqf1o  11319  bcval  11550  bcpasc  11567  hashf1lem1  11659  ccatfval  11697  ccatlid  11703  ccatass  11705  swrdid  11727  ccatswrd  11728  swrdccat2  11730  cats1un  11745  revccat  11753  revrev  11754  revco  11758  ccatco  11759  shftfn  11843  shftval  11844  limsupgle  12226  ello12  12265  elo12  12276  isercolllem3  12415  sumeq1f  12437  fsumsplit  12488  sumsplit  12507  fsum2dlem  12509  fsumcom2  12513  fsumparts  12540  explecnv  12599  eftlub  12665  divalgmod  12881  bitsval  12891  bitsp1e  12899  bitsp1o  12900  sadfval  12919  sadcp1  12922  sadval  12923  sadcadd  12925  sadadd2  12927  saddisjlem  12931  sadadd  12934  sadass  12938  smufval  12944  smuval  12948  smuval2  12949  smupvallem  12950  smu01lem  12952  smueqlem  12957  smumul  12960  bezoutlem2  12994  bezoutlem4  12996  algfx  13026  eucalgcvga  13032  unbenlem  13231  prmreclem5  13243  vdwapval  13296  vdwapun  13297  vdwnnlem1  13318  vdwnn  13321  ramval  13331  0ram  13343  ramub1lem2  13350  prmlem0  13383  elrest  13610  prdsbasmpt  13647  prdsleval  13654  prdsbasmpt2  13659  pwselbasb  13665  imasaddfnlem  13708  imasvscafn  13717  divsfval  13727  ismre  13770  mreunirn  13781  mrisval  13810  ismri  13811  isacs  13831  catidd  13860  iscatd2  13861  ismon  13914  isepi  13921  sectffval  13931  sectfval  13932  issubc  13990  isfunc  14016  funcres  14048  funcpropd  14052  ffthiso  14081  isnat  14099  isnat2  14100  fuciso  14127  arwhoma  14155  elsetchom  14191  setcmon  14197  setcepi  14198  setciso  14201  catciso  14217  hofcl  14311  hofpropd  14319  yonedalem4c  14329  yonedainv  14333  yonffthlem  14334  poslubdg  14530  acsficl2d  14557  acsmapd  14559  psref  14595  psss  14601  dirge  14637  grpidval  14662  grpidd  14673  ismndd  14674  mndpropd  14676  grpidpropd  14677  imasmnd2  14687  imasmnd  14688  ismhm  14695  issubm  14703  gsumccat  14742  imasgrp2  14888  imasgrp  14889  issubg  14899  subginv  14906  isnsg  14924  isghm  14961  resghm2b  14979  conjnmzb  14995  conjnsg  14996  ghmpropd  14998  isga  15023  elcntz  15076  elcntzsn  15079  cntzrcl  15081  resscntz  15085  gexdvds  15173  gex1  15180  isslw  15197  sylow3lem2  15217  lsmelvalx  15229  pj1ghm  15290  efgtlen  15313  efgs1b  15323  efgsfo  15326  efgredlemc  15332  frgp0  15347  frgpmhm  15352  divsabl  15435  frgpnabllem1  15439  0cyg  15457  cycsubgcyg  15465  gsumval3  15469  gsumcllem  15471  gsumzaddlem  15481  gsumzsplit  15484  eldprd  15517  dprdcntz2  15551  dprd2d2  15557  dmdprdsplit2lem  15558  dmdprdsplit2  15559  dprdsplit  15561  ablfac2  15602  isrngd  15653  imasrng  15680  dvdsrval  15705  isunit  15717  dvdsrpropd  15756  isirred  15759  isrhm  15779  drngunit  15795  isdrngd  15815  issubrg  15823  opprsubrg  15844  rhmpropd  15858  isabv  15862  issrngd  15904  islmod  15909  lmodprop2d  15961  islss  15966  islssd  15967  lssats2  16031  lspsnel  16034  islmhm  16058  lmhmf1o  16077  lmhmima  16078  lmhmpreima  16079  reslmhm  16083  lmhmpropd  16100  islbs  16103  lspprel  16121  lspfixed  16155  lbsacsbs  16183  lbsextlem1  16185  lbsextlem2  16186  lbsextlem3  16187  lbsextlem4  16188  lidlmcl  16243  divscrng  16266  islpidl  16272  lidldvgen  16281  mplsubglem  16453  mpllsslem  16454  mplmonmul  16482  mplrcl  16505  subrgascl  16513  subrgasclcl  16514  strov2rcl  16586  zrhrhmb  16747  znf1o  16787  frgpcyg  16809  isphld  16840  elocv  16850  iscss  16865  isobs  16902  obs2ss  16911  istopon  16945  eltg  16977  eltg2  16978  eltop  16994  eltop2  16995  eltop3  16996  pptbas  17027  iscld  17046  neiss2  17120  isnei  17122  neiptopnei  17151  neiptopreu  17152  lpfval  17157  lpval  17158  islp  17159  maxlp  17165  islpi  17167  neitr  17198  restlp  17201  ordtbas2  17209  ordtrest2  17222  lmfval  17250  cnfval  17251  iscn  17253  iscnp  17255  tgcn  17270  tgcnp  17271  lmbrf  17278  cnpresti  17306  ist1  17339  ist1-2  17365  cnt1  17368  haust1  17370  cmpfi  17425  cmpfii  17426  1stcfb  17461  2ndc1stc  17467  1stcrest  17469  2ndcdisj  17472  1stcelcls  17477  nllyi  17491  subislly  17497  kgenval  17520  elkgen  17521  kgencn2  17542  txbas  17552  eltx  17553  ptval  17555  ptpjpre1  17556  ptopn2  17569  ptpjopn  17597  ptclsg  17600  xkoccn  17604  txdis  17617  txdis1cn  17620  ptrescn  17624  hausdiag  17630  hauseqlcld  17631  txhaus  17632  xkohaus  17638  elqtop  17682  qtopeu  17701  kqcldsat  17718  hmeofval  17743  ptuncnv  17792  ptunhmeo  17793  elmptrab  17812  fbdmn0  17819  elfg  17856  elfilss  17861  filunirn  17867  fixufil  17907  elfm  17932  rnelfmlem  17937  rnelfm  17938  fmfnfmlem4  17942  elflim2  17949  flimtopon  17955  elflim  17956  hausflim  17966  flimcls  17970  flfnei  17976  isflf  17978  hausflf  17982  cnpflf  17986  cnflf  17987  txflf  17991  isfcls  17994  fclstopon  17997  isfcls2  17998  fclssscls  18003  fclsnei  18004  fclsfnflim  18012  flimfnfcls  18013  isfcf  18019  fcfelbas  18021  cnpfcf  18026  cnfcf  18027  alexsublem  18028  alexsubALTlem3  18033  cnextfun  18048  cnextfvval  18049  cnextf  18050  cnextcn  18051  tmdgsum2  18079  tgpconcomp  18095  ghmcnp  18097  divstgplem  18103  eltsms  18115  haustsms  18118  tsmsgsum  18121  tsmssubm  18125  tsmssplit  18134  isust  18186  elrnust  18207  ustbas  18210  elutop  18216  ustuqtoplem  18222  ustuqtop4  18227  ustuqtop  18229  utopsnneiplem  18230  utopsnneip  18231  utopsnnei  18232  isusp  18244  isucn  18261  ucncn  18268  iscfilu  18271  neipcfilu  18279  iscusp  18282  cnextucn  18286  ispsmet  18288  ismet  18306  isxmet  18307  elblps  18370  elbl  18371  elmopn  18425  prdsbl  18474  neibl  18484  met1stc  18504  metrest  18507  prdsxmslem2  18512  txmetcnp  18530  txmetcn  18531  metuvalOLD  18532  metuval  18533  metustsymOLD  18544  metustsym  18545  cfilucfil2OLD  18556  cfilucfil2  18557  elbl4  18559  metuelOLD  18560  metuel  18561  metutopOLD  18565  psmetutop  18566  restmetu  18570  metucnOLD  18571  metucn  18572  tngngp  18648  isnmhm  18733  zcld  18797  metnrmlem1a  18841  elcncf  18872  cncfcnvcn  18904  cnheibor  18933  lebnumlem1  18939  ishtpy  18950  isphtpy  18959  om1elbas  19010  elpi1  19023  pi1xfr  19033  pi1coghm  19039  tchcph  19147  lmmbrf  19168  iscfil  19171  iscau  19182  iscauf  19186  caucfil  19189  iscmet  19190  cmetcaulem  19194  iscmet3lem1  19197  iscmet3lem2  19198  iscmet3  19199  bcthlem1  19230  cmsss  19256  cmetcusp1OLD  19258  cmetcusp1  19259  cmetcuspOLD  19260  cmetcusp  19261  minveclem3b  19282  ovolfioo  19317  ovolficc  19318  ovolctb  19339  ovoliunnul  19356  ovolshftlem1  19358  sca2rab  19361  ovolscalem1  19362  ovolicc2lem1  19366  ovolicc2lem2  19367  ovolicc2lem4  19369  ovolicc2lem5  19370  iundisj  19395  iunmbl2  19404  uniioombllem3  19430  vitalilem2  19454  vitalilem3  19455  mbfss  19491  i1faddlem  19538  i1fmullem  19539  mbfi1fseqlem2  19561  mbfi1fseqlem4  19563  mbfi1fseq  19566  itg2splitlem  19593  itg2split  19594  itg2monolem1  19595  itg2gt0  19605  isibl  19610  iblss2  19650  itgss3  19659  itgsplit  19680  ellimc  19713  limcmo  19722  cnlimc  19728  limciun  19734  limcun  19735  eldv  19738  dvbsss  19742  dvreslem  19749  elcpn  19773  dvaddf  19781  dvmulf  19782  dvcof  19787  rolle  19827  dvlip2  19832  dvivthlem1  19845  lhop1  19851  lhop2  19852  ftc1cn  19880  mpfind  19918  fta1glem2  20042  plyco0  20064  elply  20067  ply1termlem  20075  eltayl  20229  tayl0  20231  taylplem1  20232  taylplem2  20233  dvtaylp  20239  taylthlem1  20242  taylthlem2  20243  abelth  20310  cxpcn3  20585  rlimcnp  20757  fsumharmonic  20803  dchrelbas  20973  pntrsumbnd2  21214  ostth2lem2  21281  usgra2edg1  21356  usgraidx2vlem1  21363  usgraidx2vlem2  21364  nbgraop  21389  nbgrael  21391  nbgraeledg  21395  nbgraf1olem1  21404  nbgraf1olem3  21406  nbgraf1olem5  21408  nbgraf1o  21410  iscusgra  21418  sizeusglecusglem1  21446  isuvtx  21450  uvtxel  21451  uvtxisvtx  21452  wlks  21479  iswlk  21480  istrl  21490  ispth  21521  isspth  21522  fargshiftlem  21574  fargshiftfv  21575  fargshiftfo  21578  vdgrfval  21619  vdgrun  21625  vdgrfiun  21626  vdgr1a  21630  eupap1  21651  eupath2lem3  21654  ex-res  21702  isabloda  21840  issubgo  21844  isass  21857  elghomlem2  21903  ghablo  21910  iscom2  21953  rngoidmlem  21964  rngo1cl  21970  isssp  22176  sspn  22188  islno  22207  isblo  22236  nmlno0  22249  ishmo  22265  dipdir  22296  dipass  22299  ubthlem1  22325  ubthlem2  22326  htthlem  22373  htth  22374  ocel  22736  ocnel  22753  shsel  22769  shsel2  22777  shmodsi  22844  pjhtheu  22849  pjeq  22854  axpjpj  22875  pjoc2  22894  elspani  22998  h1de2ctlem  23010  elspansn  23021  elspansn2  23022  elnlfn  23384  eleigvec  23413  riesz3i  23518  iuneq12daf  23960  iuneq12df  23961  iunrdx  23967  cbvdisjf  23968  disjorf  23974  disjabrex  23977  disjabrexf  23978  iundisjf  23982  disjrdx  23984  elunirn2  24016  abfmpunirn  24017  abfmpeld  24019  abfmpel  24020  fmptdF  24022  fmptcof2  24029  funcnvmptOLD  24035  funcnvmpt  24036  xrofsup  24079  iundisjfi  24105  eliccioo  24130  xrge0tsmsbi  24177  inftmrel  24203  isinftm  24204  metidval  24238  pstmval  24243  cnre2csqima  24262  fmcncfil  24270  ofcfval  24434  measvuni  24521  meascnbl  24526  faeval  24550  ismbfm  24555  elunirnmbfm  24556  isanmbfm  24559  imambfm  24565  itgeq12dv  24594  issibf  24601  rrvmbfm  24653  elorvc  24670  elorrvc  24674  dstfrvunirn  24685  ballotlemfc0  24703  ballotlemfcc  24704  ballotlemsima  24726  ballotlemrv  24730  subfacp1lem2b  24820  subfacp1lem4  24822  subfacp1lem5  24823  subfacp1lem6  24824  ptpcon  24873  cvmscbv  24898  iscvm  24899  cvmsi  24905  cvmsval  24906  cvmliftmolem1  24921  cvmlift2lem12  24954  cvmlift2lem13  24955  cvmlift3lem7  24965  snmlval  24971  elgiso  25060  fprodser  25228  fprodsplit  25242  fprod2dlem  25257  fprodcom2  25261  mpteq12d  25342  predbrg  25400  trpredrec  25455  wfrlem9  25478  wfrlem12  25481  fvnobday  25550  nodenselem3  25551  nodenselem5  25553  nofulllem5  25574  elee  25737  brbtwn  25742  brcgr  25743  axlowdimlem16  25800  funtransport  25869  fvtransport  25870  brcolinear  25897  colineardim1  25899  funray  25978  fvray  25979  funline  25980  fvline  25982  lineelsb2  25986  rankelg  26013  rankeq1o  26016  elhf2  26020  0hf  26022  mblfinlem  26143  volsupnfl  26150  itg2addnclem  26155  itg2gt0cn  26159  islocfin  26266  lfinpfin  26273  locfindis  26275  locfincf  26276  comppfsc  26277  neibastop2lem  26279  neibastop3  26281  eltail  26293  indexdom  26326  incsequz  26342  istotbnd  26368  istotbnd3  26370  0totbnd  26372  sstotbnd  26374  sstotbnd3  26375  isbnd  26379  prdstotbnd  26393  cntotbnd  26395  isismty  26400  heibor1lem  26408  heiborlem2  26411  heiborlem3  26412  heibor  26420  exidcl  26441  exidreslem  26442  divrngcl  26463  isdrngo2  26464  isrngohom  26471  isrngoiso  26484  isriscg  26490  iscringd  26499  isidl  26514  ispridl  26534  ismaxidl  26540  prter3  26621  fnelfp  26626  fnelnfp  26628  isnacs  26648  mrefg2  26651  elmzpcl  26673  mzpcompact2  26699  eldiophb  26705  elpell1qr  26800  elpell14qr  26802  elpell1234qr  26804  pw2f1ocnv  26998  pw2f1o2val2  27001  aomclem4  27022  aomclem6  27024  islssfg2  27037  pwssplit3  27058  dsmmbas2  27071  dsmmfi  27072  dsmmelbas  27073  dsmmlss  27078  frlmelbas  27092  frlmlbs  27117  frlmup1  27118  ellspd  27122  imasgim  27132  islinds  27147  islindf2  27152  f1lindf  27160  islindf4  27176  lnr2i  27188  elmnc  27209  rngunsnply  27246  f1otrspeq  27258  pmtrfrn  27268  psgnunilem1  27284  psgnunilem5  27285  psgnunilem2  27286  psgnunilem3  27287  psgneldm2  27295  mat1  27350  issdrg  27373  dvconstbi  27419  stoweidlem27  27643  stoweidlem29  27645  stoweidlem31  27647  stoweidlem34  27650  stoweidlem48  27664  stoweidlem59  27675  afvelrnb  27894  afvelrnb0  27895  ubmelfzo  27986  elfzelfzccat  28006  swrd0swrd  28009  swrdswrd  28011  swrdswrd0  28013  swrdccatin1  28016  swrdccatin2  28018  swrdccatin12lem2  28020  swrdccatin12lem3b  28022  swrdccatin12lem3c  28023  swrdccatin12lem3  28024  swrdccatin12  28026  swrdccatin12b  28027  swrdccat3  28029  swrdccat3b  28031  usgra2pthlem1  28040  2wlksot  28064  2spthsot  28065  el2wlkonot  28066  el2spthonot  28067  el2spthonot0  28068  2wlkonot3v  28072  2spthonot3v  28073  el2wlksoton  28075  el2spthsoton  28076  el2wlksotot  28079  usg2spthonot  28085  usg2spthonot0  28086  frgrancvvdeqlem3  28135  usg2spot2nb  28168  usgreg2spot  28170  2spotmdisj  28171  bnj945  28850  bnj1400  28913  bnj18eq1  29004  bnj916  29010  bnj1014  29037  bnj1015  29038  bnj1110  29057  bnj1417  29116  islshp  29462  islsat  29474  lcvfbr  29503  islfl  29543  ellkr  29572  islshpkrN  29603  ldual1dim  29649  isopos  29663  cmtfvalN  29693  cvrfval  29751  isat  29769  islln  29988  islpln  30012  islvol  30055  isline  30221  ispointN  30224  ispsubsp  30227  elpmap  30240  elpmapat  30246  elpadd  30281  paddclN  30324  elpclN  30374  elpcliN  30375  pclfinN  30382  pclcmpatN  30383  ispsubclN  30419  iswatN  30476  islhp  30478  islaut  30565  ispautN  30581  isldil  30592  isltrn  30601  isdilN  30636  istrnN  30639  istendo  31242  dvhb1dimN  31468  erng1lem  31469  erngdvlem4-rN  31481  diaelval  31516  diaeldm  31519  dia1dimid  31546  cdlemm10N  31601  dibopelvalN  31626  dibopelval2  31628  dibelval3  31630  dibelval1st  31632  dibelval2nd  31635  dibeldmN  31641  dibvalrel  31646  dibglbN  31649  dicffval  31657  dicfval  31658  dicopelval  31660  dicelvalN  31661  dicelval3  31663  dicvalrelN  31668  dicelval1sta  31670  diclspsn  31677  dihopelvalbN  31721  dihopelvalcqat  31729  dihopelvalcpre  31731  dihvalrel  31762  dih1  31769  dihmeetlem4preN  31789  dihmeetlem13N  31802  dih1dimatlem  31812  dochnel2  31875  dihjatcclem4  31904  dvh2dim  31928  dvh3dim  31929  dvh4dimN  31930  dochfln0  31960  lpolsetN  31965  islpolN  31966  lcfrvalsnN  32024  lcfrlem21  32046  lcfrlem27  32052  lcfrlem37  32062  lcfr  32068  lcdlss  32102  mapdcv  32143  hdmap1fval  32280  hdmapffval  32312  hdmapfval  32313  hdmapval  32314  hgmapffval  32371  hgmapfval  32372  hdmapellkr  32400  hlhilhillem  32446
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 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2397  df-clel 2400
  Copyright terms: Public domain W3C validator