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

Theorem eleq2d 2352
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 2346 . 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 1625    e. wcel 1686
This theorem is referenced by:  eleq12d  2353  eleqtrd  2361  neleqtrd  2380  neleqtrrd  2381  abeq2d  2394  nfceqdf  2420  drnfc1  2437  drnfc2  2438  sbcbid  3046  cbvcsb  3087  sbcel1g  3102  csbeq2d  3107  csbie2g  3129  cbvralcsf  3145  cbvreucsf  3147  cbvrabcsf  3148  cbviun  3941  cbviin  3942  iinxsng  3980  iinxprg  3981  iunxsng  3982  cbvdisj  4005  disjor  4009  mpteq12f  4098  axpweq  4189  rabxfrd  4557  0nelelxp  4720  opeliunxp  4742  opeliunxp2  4826  iunxpf  4834  elrelimasn  5039  elimasng  5041  elimasni  5042  ressn  5213  funfni  5346  fnbr  5348  fun11iun  5495  dffv3  5523  fvelrnb  5572  fvun1  5592  fvco2  5596  elpreima  5647  dff3  5675  fmptco  5693  zfrep6  5750  funfvima3  5757  eluniima  5778  dff13  5785  f1eqcocnv  5807  isoini  5837  mpt2eq123dva  5911  cbvmpt2x  5926  ovelrn  5998  elovmpt2  6066  fmpt2x  6192  rntpos  6249  riotaeqdv  6307  onoviun  6362  smoel  6379  smoiso  6381  smoel2  6382  smo11  6383  smoord  6384  tfrlem9  6403  oalimcl  6560  oaass  6561  omordi  6566  omordlim  6577  omlimcl  6578  odi  6579  omeulem1  6582  omeulem2  6583  omopth2  6584  oen0  6586  oeordi  6587  oeordsuc  6594  oelimcl  6600  oeeulem  6601  oeeui  6602  nnmordi  6631  oaabs2  6645  omabs  6647  omsmolem  6653  ereldm  6705  iiner  6733  elmapg  6787  elpmg  6788  elixpsn  6857  ixpsnf1o  6858  boxriin  6860  omxpenlem  6965  pw2f1olem  6968  phplem4  7045  php3  7049  elfi  7169  dffi3  7186  marypha2lem2  7191  ordiso2  7232  wemapso2lem  7267  elharval  7279  inf3lemd  7330  inf3lem1  7331  inf3lem2  7332  inf3lem3  7333  cantnfs  7369  cantnfp1lem3  7384  cantnflem1b  7390  cantnflem1  7393  trcl  7412  r1sdom  7448  r1ordg  7452  r1pwss  7458  tz9.12lem3  7463  tz9.12  7464  r1elwf  7470  rankr1ai  7472  rankidb  7474  rankr1bg  7477  rankval2  7492  rankunb  7524  tcrank  7556  fseqdom  7655  acni  7674  acni2  7675  acndom  7680  infpwfien  7691  alephnbtwn  7700  cardaleph  7718  cardinfima  7726  iunfictbso  7743  dfac3  7750  dfac5lem5  7756  dfac5  7757  dfac9  7764  dfac12r  7774  kmlem2  7779  kmlem12  7789  kmlem13  7790  kmlem14  7791  ackbij2lem3  7869  ackbij2  7871  cofsmo  7897  cfsmolem  7898  alephsing  7904  fin23lem30  7970  isf32lem9  7989  itunisuc  8047  axcc2lem  8064  axcc3  8066  domtriomlem  8070  axdc2lem  8076  axdc2  8077  axdc3lem2  8079  axdc3lem4  8081  axdc4lem  8083  ac6c4  8110  zorn2lem1  8125  ttukeylem6  8143  pwcfsdom  8207  axregndlem2  8227  axinfndlem1  8229  axacndlem4  8234  axacnd  8236  pwfseqlem1  8282  inar1  8399  inatsk  8402  r1tskina  8406  gruurn  8422  grur1  8444  grothpw  8450  eltskm  8467  genpelv  8626  eluz1  10236  eluzadd  10258  eluzsub  10259  elixx1  10667  elixx3g  10671  elioo2  10699  elfz1  10789  elfz2  10791  elfzp1  10838  fzpr  10842  fzsuc2  10844  fzrev3  10851  elfzp12  10863  elfzo  10879  elfzom1b  10920  fzosplitsni  10923  seqp1  11063  seqf1o  11089  bcval  11319  bcpasc  11335  hashf1lem1  11395  ccatfval  11430  ccatlid  11436  ccatass  11438  swrdid  11460  ccatswrd  11461  swrdccat2  11463  cats1un  11478  revccat  11486  revrev  11487  revco  11491  ccatco  11492  shftfn  11570  shftval  11571  limsupgle  11953  ello12  11992  elo12  12003  isercolllem3  12142  sumeq1f  12163  cbvsum  12170  fsumsplit  12214  sumsplit  12233  fsum2dlem  12235  fsumcom2  12239  fsumparts  12266  explecnv  12325  eftlub  12391  divalgmod  12607  bitsval  12617  bitsp1e  12625  bitsp1o  12626  sadfval  12645  sadcp1  12648  sadval  12649  sadcadd  12651  sadadd2  12653  saddisjlem  12657  sadadd  12660  sadass  12664  smufval  12670  smuval  12674  smuval2  12675  smupvallem  12676  smu01lem  12678  smueqlem  12683  smumul  12686  bezoutlem2  12720  bezoutlem4  12722  algfx  12752  eucalgcvga  12758  unbenlem  12957  prmreclem5  12969  vdwapval  13022  vdwapun  13023  vdwnnlem1  13044  vdwnn  13047  ramval  13057  0ram  13069  ramub1lem2  13076  prmlem0  13109  elrest  13334  prdsbasmpt  13371  prdsleval  13378  prdsbasmpt2  13383  pwselbasb  13389  imasaddfnlem  13432  imasvscafn  13441  divsfval  13451  ismre  13494  mreunirn  13505  mrisval  13534  ismri  13535  isacs  13555  catidd  13584  iscatd2  13585  ismon  13638  isepi  13645  sectffval  13655  sectfval  13656  issubc  13714  isfunc  13740  funcres  13772  funcpropd  13776  ffthiso  13805  isnat  13823  isnat2  13824  fuciso  13851  arwhoma  13879  elsetchom  13915  setcmon  13921  setcepi  13922  setciso  13925  catciso  13941  hofcl  14035  hofpropd  14043  yonedalem4c  14053  yonedainv  14057  yonffthlem  14058  poslubdg  14254  acsficl2d  14281  acsmapd  14283  psref  14319  psss  14325  dirge  14361  grpidval  14386  grpidd  14397  ismndd  14398  mndpropd  14400  grpidpropd  14401  imasmnd2  14411  imasmnd  14412  ismhm  14419  issubm  14427  gsumccat  14466  imasgrp2  14612  imasgrp  14613  issubg  14623  subginv  14630  isnsg  14648  isghm  14685  resghm2b  14703  conjnmzb  14719  conjnsg  14720  ghmpropd  14722  isga  14747  elcntz  14800  elcntzsn  14803  cntzrcl  14805  resscntz  14809  gexdvds  14897  gex1  14904  isslw  14921  sylow3lem2  14941  lsmelvalx  14953  pj1ghm  15014  efgtlen  15037  efgs1b  15047  efgsfo  15050  efgredlemc  15056  frgp0  15071  frgpmhm  15076  divsabl  15159  frgpnabllem1  15163  0cyg  15181  cycsubgcyg  15189  gsumval3  15193  gsumcllem  15195  gsumzaddlem  15205  gsumzsplit  15208  eldprd  15241  dprdcntz2  15275  dprd2d2  15281  dmdprdsplit2lem  15282  dmdprdsplit2  15283  dprdsplit  15285  ablfac2  15326  isrngd  15377  imasrng  15404  dvdsrval  15429  isunit  15441  dvdsrpropd  15480  isirred  15483  isrhm  15503  drngunit  15519  isdrngd  15539  issubrg  15547  opprsubrg  15568  rhmpropd  15582  isabv  15586  issrngd  15628  islmod  15633  lmodprop2d  15689  islss  15694  islssd  15695  lssats2  15759  lspsnel  15762  islmhm  15786  lmhmf1o  15805  lmhmima  15806  lmhmpreima  15807  reslmhm  15811  lmhmpropd  15828  islbs  15831  lspprel  15849  lspfixed  15883  lspindp4  15892  lsppratlem3  15904  lbsacsbs  15911  lbsextlem1  15913  lbsextlem2  15914  lbsextlem3  15915  lbsextlem4  15916  lidlmcl  15971  divscrng  15994  islpidl  16000  lidldvgen  16009  mplsubglem  16181  mpllsslem  16182  mplmonmul  16210  mplrcl  16233  subrgascl  16241  subrgasclcl  16242  strov2rcl  16317  zrhrhmb  16467  znf1o  16507  frgpcyg  16529  isphld  16560  elocv  16570  iscss  16585  isobs  16622  obs2ss  16631  istopon  16665  eltg  16697  eltg2  16698  eltop  16714  eltop2  16715  eltop3  16716  pptbas  16747  iscld  16766  neiss2  16840  isnei  16842  lpfval  16872  lpval  16873  islp  16874  maxlp  16880  islpi  16882  restlp  16915  ordtbas2  16923  ordtrest2  16936  lmfval  16964  cnfval  16965  iscn  16967  iscnp  16969  tgcn  16984  tgcnp  16985  lmbrf  16992  cnpresti  17018  ist1  17051  ist1-2  17077  cnt1  17080  haust1  17082  cmpfi  17137  cmpfii  17138  1stcfb  17173  2ndc1stc  17179  1stcrest  17181  2ndcdisj  17184  1stcelcls  17189  nllyi  17203  subislly  17209  kgenval  17232  elkgen  17233  kgencn2  17254  txbas  17264  eltx  17265  ptval  17267  ptpjpre1  17268  ptopn2  17281  ptpjopn  17308  ptclsg  17311  xkoccn  17315  txdis  17328  txdis1cn  17331  ptrescn  17335  hausdiag  17341  hauseqlcld  17342  txhaus  17343  xkohaus  17349  elqtop  17390  qtopeu  17409  kqcldsat  17426  hmeofval  17451  ptuncnv  17500  ptunhmeo  17501  elmptrab  17524  fbdmn0  17531  elfg  17568  elfilss  17573  filunirn  17579  fixufil  17619  elfm  17644  rnelfmlem  17649  rnelfm  17650  fmfnfmlem4  17654  elflim2  17661  flimtopon  17667  elflim  17668  hausflim  17678  flimcls  17682  flfnei  17688  isflf  17690  hausflf  17694  cnpflf  17698  cnflf  17699  txflf  17703  isfcls  17706  fclstopon  17709  isfcls2  17710  fclssscls  17715  fclsnei  17716  fclsfnflim  17724  flimfnfcls  17725  isfcf  17731  fcfelbas  17733  cnpfcf  17738  cnfcf  17739  alexsublem  17740  alexsubALTlem3  17745  tmdgsum2  17781  tgpconcomp  17797  ghmcnp  17799  divstgplem  17805  eltsms  17817  haustsms  17820  tsmsgsum  17823  tsmssubm  17827  tsmssplit  17836  ismet  17890  isxmet  17891  elbl  17951  elmopn  17990  prdsbl  18039  neibl  18049  met1stc  18069  metrest  18072  prdsxmslem2  18077  txmetcnp  18095  txmetcn  18096  tngngp  18172  isnmhm  18257  zcld  18321  metnrmlem1a  18364  elcncf  18395  cncfcnvcn  18426  cnheibor  18455  lebnumlem1  18461  ishtpy  18472  isphtpy  18481  om1elbas  18532  elpi1  18545  pi1xfr  18555  pi1coghm  18561  tchcph  18669  lmmbrf  18690  iscfil  18693  iscau  18704  iscauf  18708  caucfil  18711  iscmet  18712  cmetcaulem  18716  iscmet3lem1  18719  iscmet3lem2  18720  iscmet3  18721  bcthlem1  18748  cmsss  18774  minveclem3b  18794  ovolfioo  18829  ovolficc  18830  ovolctb  18851  ovoliunnul  18868  ovolshftlem1  18870  sca2rab  18873  ovolscalem1  18874  ovolicc2lem1  18878  ovolicc2lem2  18879  ovolicc2lem4  18881  ovolicc2lem5  18882  iundisj  18907  iunmbl2  18916  uniioombllem3  18942  vitalilem2  18966  vitalilem3  18967  mbfss  19003  i1faddlem  19050  i1fmullem  19051  mbfi1fseqlem2  19073  mbfi1fseqlem4  19075  mbfi1fseq  19078  itg2splitlem  19105  itg2split  19106  itg2monolem1  19107  itg2gt0  19117  isibl  19122  iblss2  19162  itgss3  19171  itgsplit  19192  ellimc  19225  limcmo  19234  cnlimc  19240  limciun  19246  limcun  19247  eldv  19250  dvbsss  19254  dvreslem  19261  elcpn  19285  dvaddf  19293  dvmulf  19294  dvcof  19299  rolle  19339  dvlip2  19344  dvivthlem1  19357  lhop1  19363  lhop2  19364  ftc1cn  19392  mpfind  19430  fta1glem2  19554  plyco0  19576  elply  19579  ply1termlem  19587  eltayl  19741  tayl0  19743  taylplem1  19744  taylplem2  19745  dvtaylp  19751  taylthlem1  19754  taylthlem2  19755  abelth  19819  cxpcn3  20090  rlimcnp  20262  fsumharmonic  20307  dchrelbas  20477  pntrsumbnd2  20718  ostth2lem2  20785  ex-res  20830  isabloda  20968  issubgo  20972  isass  20985  elghomlem2  21031  ghablo  21038  iscom2  21081  rngoidmlem  21092  rngo1cl  21098  isssp  21302  sspn  21314  islno  21333  isblo  21362  nmlno0  21375  ishmo  21391  dipdir  21422  dipass  21425  ubthlem1  21451  ubthlem2  21452  htthlem  21499  htth  21500  ocel  21862  ocnel  21879  shsel  21895  shsel2  21903  shmodsi  21970  pjhtheu  21975  pjeq  21980  axpjpj  22001  pjoc2  22020  elspani  22124  h1de2ctlem  22136  elspansn  22147  elspansn2  22148  elnlfn  22510  eleigvec  22539  riesz3i  22644  ballotlemfc0  23053  ballotlemfcc  23054  ballotlemsima  23076  ballotlemrv  23080  eliccioo  23117  iuneq12daf  23156  iuneq12df  23157  iunrdx  23163  itgeq12dv  23198  elunirn2  23217  fmptdF  23223  fmptcof2  23231  funcnvmptOLD  23236  funcnvmpt  23237  xrofsup  23257  cnre2csqima  23297  cbvdisjf  23352  disjorf  23358  disjabrex  23361  disjabrexf  23362  iundisjfi  23365  iundisjf  23367  disjrdx  23372  xrge0tsmsbi  23385  ofcfval  23461  measvuni  23544  measiuns  23546  meascnbl  23548  ismbfm  23559  elunirnmbfm  23560  isanmbfm  23563  imambfm  23569  dya2iocrrnval  23584  probfinmeasb  23634  rrvmbfm  23647  elorvc  23662  elorrvc  23666  dstrvprob  23674  dstfrvel  23676  dstfrvunirn  23677  subfacp1lem2b  23714  subfacp1lem4  23716  subfacp1lem5  23717  subfacp1lem6  23718  ptpcon  23766  cvmscbv  23791  iscvm  23792  cvmsi  23798  cvmsval  23799  cvmliftmolem1  23814  cvmlift2lem12  23847  cvmlift2lem13  23848  cvmlift3lem7  23858  vdgrfval  23891  vdgrun  23895  vdgr1a  23899  eupap1  23902  eupath2lem3  23905  snmlval  23916  elgiso  24005  mpteq12d  24130  predbrg  24188  trpredrec  24243  wfrlem9  24266  wfrlem12  24269  fvnobday  24338  nodenselem3  24339  nodenselem5  24341  nofulllem5  24362  elee  24524  brbtwn  24529  brcgr  24530  axlowdimlem16  24587  funtransport  24656  fvtransport  24657  brcolinear  24684  colineardim1  24686  funray  24765  fvray  24766  funline  24767  fvline  24769  lineelsb2  24773  rankelg  24800  rankeq1o  24803  elhf2  24807  0hf  24809  itg2addnclem  24933  domrngref  25071  repfuntw  25171  repcpwti  25172  dstr  25182  iscst3  25187  islatalg  25194  valcurfn1  25215  isorhom  25222  isoriso2  25224  puub2  25269  puub  25270  mxlelt  25275  ismxl2  25278  ismnl2  25279  isdir2  25303  prodeq2  25318  prodeq3ii  25319  dffprod  25330  iscom  25344  clfsebsr  25360  imtr  25409  prsubrtr  25410  isfldOLD  25437  idlvalNEW  25456  isidlNEW  25457  basexre  25533  nsn  25541  intopcoaconb  25551  usptoplem  25557  istopx  25558  usptop  25561  prcnt  25562  filint2  25564  conttnf2  25573  limptlimpr2lem1  25585  limptlimpr2lem2  25586  altretop  25611  iintlem1  25621  supnuf  25640  cnegvex2b  25673  rnegvex2b  25674  isded  25747  dedi  25748  iscatOLD  25765  cati  25766  dualded  25794  dualcat2  25795  ishomc  25800  ishomd  25801  ismonb  25821  imonclem  25824  isepib  25831  iepiclem  25834  isfuna  25845  isfunb  25846  issubcata  25857  idsubfun  25869  isinob  25873  issrc  25878  propsrc  25879  isntr  25884  islimcat  25887  vtarsuelt  25906  prismorcset  25925  prismorcset2  25929  domcatfun  25936  codcatfun  25945  prismorcset3  25949  isrocatset  25968  cmppar3  25985  setiscat  25990  isnword  25997  1iskle  26000  indcls2  26007  empklst  26020  clscnc  26021  phckle  26038  psckle  26039  fnckle  26056  cndpv  26060  pgapspf  26063  pgapspf2  26064  lineval22  26093  lineval2a  26096  lineval2b  26097  lineval5a  26099  lineval6a  26100  iscol2  26104  isconcl2b  26109  isibg2  26121  isibg2aa  26123  isibg2aalem1  26124  isibg2aalem2  26125  sgplpte21  26143  sgplpte22  26149  sgplpte21d1  26150  sgplpte21d2  26151  lppotoslem  26154  isray2  26164  isray  26165  isside0  26175  abhp  26184  abhp1  26185  isibcg  26202  islocfin  26307  lfinpfin  26314  locfindis  26316  locfincf  26317  comppfsc  26318  neibastop2lem  26320  neibastop3  26322  eltail  26334  indexdom  26424  incsequz  26469  istotbnd  26504  istotbnd3  26506  0totbnd  26508  sstotbnd  26510  sstotbnd3  26511  isbnd  26515  prdstotbnd  26529  cntotbnd  26531  isismty  26536  heibor1lem  26544  heiborlem2  26547  heiborlem3  26548  heibor  26556  exidcl  26577  exidreslem  26578  divrngcl  26599  isdrngo2  26600  isrngohom  26607  isrngoiso  26620  isriscg  26626  iscringd  26635  isidl  26650  ispridl  26670  ismaxidl  26676  prter3  26761  fnelfp  26766  fnelnfp  26768  isnacs  26790  mrefg2  26793  elmzpcl  26815  mzpcompact2  26841  eldiophb  26847  elpell1qr  26943  elpell14qr  26945  elpell1234qr  26947  pw2f1ocnv  27141  pw2f1o2val2  27144  aomclem4  27165  aomclem6  27167  islssfg2  27180  pwssplit3  27201  dsmmbas2  27214  dsmmfi  27215  dsmmelbas  27216  dsmmlss  27221  frlmelbas  27235  frlmlbs  27260  frlmup1  27261  ellspd  27265  imasgim  27275  islinds  27290  islindf2  27295  f1lindf  27303  islindf4  27319  lnr2i  27331  elmnc  27352  rngunsnply  27389  f1otrspeq  27401  pmtrfrn  27411  psgnunilem1  27427  psgnunilem5  27428  psgnunilem2  27429  psgnunilem3  27430  psgneldm2  27438  mat1  27493  issdrg  27516  dvconstbi  27562  fnchoice  27711  rfcnpre3  27715  rfcnpre4  27716  fmul01lt1lem2  27726  stoweidlem11  27771  stoweidlem26  27786  stoweidlem27  27787  stoweidlem29  27789  stoweidlem31  27791  stoweidlem34  27794  stoweidlem48  27808  stoweidlem57  27817  stoweidlem59  27819  afvelrnb  28036  afvelrnb0  28037  mpt2xopn0yelv  28090  mpt2xopovel  28097  nbgraop  28151  nbgrael  28152  nbusgra  28154  nbgraeledg  28156  iscusgra  28164  isuvtx  28171  uvtxel  28172  uvtxisvtx  28173  bnj945  28878  bnj1400  28941  bnj18eq1  29032  bnj916  29038  bnj1014  29065  bnj1015  29066  bnj1110  29085  bnj1417  29144  islshp  29242  islsat  29254  lcvfbr  29283  islfl  29323  ellkr  29352  islshpkrN  29383  ldual1dim  29429  isopos  29443  cmtfvalN  29473  cvrfval  29531  isat  29549  islln  29768  islpln  29792  islvol  29835  isline  30001  ispointN  30004  ispsubsp  30007  elpmap  30020  elpmapat  30026  elpadd  30061  paddclN  30104  elpclN  30154  elpcliN  30155  pclfinN  30162  pclcmpatN  30163  ispsubclN  30199  iswatN  30256  islhp  30258  islaut  30345  ispautN  30361  isldil  30372  isltrn  30381  isdilN  30416  istrnN  30419  istendo  31022  dvhb1dimN  31248  erng1lem  31249  erngdvlem4-rN  31261  diaelval  31296  diaeldm  31299  dia1dimid  31326  cdlemm10N  31381  dibopelvalN  31406  dibopelval2  31408  dibelval3  31410  dibelval1st  31412  dibelval2nd  31415  dibeldmN  31421  dibvalrel  31426  dibglbN  31429  dicffval  31437  dicfval  31438  dicopelval  31440  dicelvalN  31441  dicelval3  31443  dicvalrelN  31448  dicelval1sta  31450  diclspsn  31457  dihopelvalbN  31501  dihopelvalcqat  31509  dihopelvalcpre  31511  dihvalrel  31542  dih1  31549  dihmeetlem4preN  31569  dihmeetlem13N  31582  dih1dimatlem  31592  dochnel2  31655  dochnel  31656  dihjatcclem4  31684  dvh2dim  31708  dvh3dim  31709  dvh4dimN  31710  dochfln0  31740  lpolsetN  31745  islpolN  31746  lcfrvalsnN  31804  lcfrlem21  31826  lcfrlem27  31832  lcfrlem37  31842  lcfr  31848  lcdlss  31882  mapdcv  31923  mapdindp2  31984  mapdindp4  31986  mapdh6dN  32002  hdmap1fval  32060  hdmap1l6d  32077  hdmapffval  32092  hdmapfval  32093  hdmapval  32094  hgmapffval  32151  hgmapfval  32152  hdmapellkr  32180  hlhilhillem  32226
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-11 1717  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1531  df-cleq 2278  df-clel 2281
  Copyright terms: Public domain W3C validator