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

Theorem eleq2d 2350
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 2344 . 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 1623    e. wcel 1684
This theorem is referenced by:  eleq12d  2351  eleqtrd  2359  neleqtrd  2378  neleqtrrd  2379  abeq2d  2392  nfceqdf  2418  drnfc1  2435  drnfc2  2436  sbcbid  3044  cbvcsb  3085  sbcel1g  3100  csbeq2d  3105  csbie2g  3127  cbvralcsf  3143  cbvreucsf  3145  cbvrabcsf  3146  cbviun  3939  cbviin  3940  iinxsng  3978  iinxprg  3979  iunxsng  3980  cbvdisj  4003  disjor  4007  mpteq12f  4096  axpweq  4187  rabxfrd  4555  0nelelxp  4718  opeliunxp  4740  opeliunxp2  4824  iunxpf  4832  elrelimasn  5037  elimasng  5039  elimasni  5040  ressn  5211  funfni  5344  fnbr  5346  fun11iun  5493  dffv3  5521  fvelrnb  5570  fvun1  5590  fvco2  5594  elpreima  5645  dff3  5673  fmptco  5691  zfrep6  5748  funfvima3  5755  eluniima  5776  dff13  5783  f1eqcocnv  5805  isoini  5835  mpt2eq123dva  5909  cbvmpt2x  5924  ovelrn  5996  elovmpt2  6064  fmpt2x  6190  rntpos  6247  riotaeqdv  6305  onoviun  6360  smoel  6377  smoiso  6379  smoel2  6380  smo11  6381  smoord  6382  tfrlem9  6401  oalimcl  6558  oaass  6559  omordi  6564  omordlim  6575  omlimcl  6576  odi  6577  omeulem1  6580  omeulem2  6581  omopth2  6582  oen0  6584  oeordi  6585  oeordsuc  6592  oelimcl  6598  oeeulem  6599  oeeui  6600  nnmordi  6629  oaabs2  6643  omabs  6645  omsmolem  6651  ereldm  6703  iiner  6731  elmapg  6785  elpmg  6786  elixpsn  6855  ixpsnf1o  6856  boxriin  6858  omxpenlem  6963  pw2f1olem  6966  phplem4  7043  php3  7047  elfi  7167  dffi3  7184  marypha2lem2  7189  ordiso2  7230  wemapso2lem  7265  elharval  7277  inf3lemd  7328  inf3lem1  7329  inf3lem2  7330  inf3lem3  7331  cantnfs  7367  cantnfp1lem3  7382  cantnflem1b  7388  cantnflem1  7391  trcl  7410  r1sdom  7446  r1ordg  7450  r1pwss  7456  tz9.12lem3  7461  tz9.12  7462  r1elwf  7468  rankr1ai  7470  rankidb  7472  rankr1bg  7475  rankval2  7490  rankunb  7522  tcrank  7554  fseqdom  7653  acni  7672  acni2  7673  acndom  7678  infpwfien  7689  alephnbtwn  7698  cardaleph  7716  cardinfima  7724  iunfictbso  7741  dfac3  7748  dfac5lem5  7754  dfac5  7755  dfac9  7762  dfac12r  7772  kmlem2  7777  kmlem12  7787  kmlem13  7788  kmlem14  7789  ackbij2lem3  7867  ackbij2  7869  cofsmo  7895  cfsmolem  7896  alephsing  7902  fin23lem30  7968  isf32lem9  7987  itunisuc  8045  axcc2lem  8062  axcc3  8064  domtriomlem  8068  axdc2lem  8074  axdc2  8075  axdc3lem2  8077  axdc3lem4  8079  axdc4lem  8081  ac6c4  8108  zorn2lem1  8123  ttukeylem6  8141  pwcfsdom  8205  axregndlem2  8225  axinfndlem1  8227  axacndlem4  8232  axacnd  8234  pwfseqlem1  8280  inar1  8397  inatsk  8400  r1tskina  8404  gruurn  8420  grur1  8442  grothpw  8448  eltskm  8465  genpelv  8624  eluz1  10234  eluzadd  10256  eluzsub  10257  elixx1  10665  elixx3g  10669  elioo2  10697  elfz1  10787  elfz2  10789  elfzp1  10836  fzpr  10840  fzsuc2  10842  fzrev3  10849  elfzp12  10861  elfzo  10877  elfzom1b  10918  fzosplitsni  10921  seqp1  11061  seqf1o  11087  bcval  11317  bcpasc  11333  hashf1lem1  11393  ccatfval  11428  ccatlid  11434  ccatass  11436  swrdid  11458  ccatswrd  11459  swrdccat2  11461  cats1un  11476  revccat  11484  revrev  11485  revco  11489  ccatco  11490  shftfn  11568  shftval  11569  limsupgle  11951  ello12  11990  elo12  12001  isercolllem3  12140  sumeq1f  12161  cbvsum  12168  fsumsplit  12212  sumsplit  12231  fsum2dlem  12233  fsumcom2  12237  fsumparts  12264  explecnv  12323  eftlub  12389  divalgmod  12605  bitsval  12615  bitsp1e  12623  bitsp1o  12624  sadfval  12643  sadcp1  12646  sadval  12647  sadcadd  12649  sadadd2  12651  saddisjlem  12655  sadadd  12658  sadass  12662  smufval  12668  smuval  12672  smuval2  12673  smupvallem  12674  smu01lem  12676  smueqlem  12681  smumul  12684  bezoutlem2  12718  bezoutlem4  12720  algfx  12750  eucalgcvga  12756  unbenlem  12955  prmreclem5  12967  vdwapval  13020  vdwapun  13021  vdwnnlem1  13042  vdwnn  13045  ramval  13055  0ram  13067  ramub1lem2  13074  prmlem0  13107  elrest  13332  prdsbasmpt  13369  prdsleval  13376  prdsbasmpt2  13381  pwselbasb  13387  imasaddfnlem  13430  imasvscafn  13439  divsfval  13449  ismre  13492  mreunirn  13503  mrisval  13532  ismri  13533  isacs  13553  catidd  13582  iscatd2  13583  ismon  13636  isepi  13643  sectffval  13653  sectfval  13654  issubc  13712  isfunc  13738  funcres  13770  funcpropd  13774  ffthiso  13803  isnat  13821  isnat2  13822  fuciso  13849  arwhoma  13877  elsetchom  13913  setcmon  13919  setcepi  13920  setciso  13923  catciso  13939  hofcl  14033  hofpropd  14041  yonedalem4c  14051  yonedainv  14055  yonffthlem  14056  poslubdg  14252  acsficl2d  14279  acsmapd  14281  psref  14317  psss  14323  dirge  14359  grpidval  14384  grpidd  14395  ismndd  14396  mndpropd  14398  grpidpropd  14399  imasmnd2  14409  imasmnd  14410  ismhm  14417  issubm  14425  gsumccat  14464  imasgrp2  14610  imasgrp  14611  issubg  14621  subginv  14628  isnsg  14646  isghm  14683  resghm2b  14701  conjnmzb  14717  conjnsg  14718  ghmpropd  14720  isga  14745  elcntz  14798  elcntzsn  14801  cntzrcl  14803  resscntz  14807  gexdvds  14895  gex1  14902  isslw  14919  sylow3lem2  14939  lsmelvalx  14951  pj1ghm  15012  efgtlen  15035  efgs1b  15045  efgsfo  15048  efgredlemc  15054  frgp0  15069  frgpmhm  15074  divsabl  15157  frgpnabllem1  15161  0cyg  15179  cycsubgcyg  15187  gsumval3  15191  gsumcllem  15193  gsumzaddlem  15203  gsumzsplit  15206  eldprd  15239  dprdcntz2  15273  dprd2d2  15279  dmdprdsplit2lem  15280  dmdprdsplit2  15281  dprdsplit  15283  ablfac2  15324  isrngd  15375  imasrng  15402  dvdsrval  15427  isunit  15439  dvdsrpropd  15478  isirred  15481  isrhm  15501  drngunit  15517  isdrngd  15537  issubrg  15545  opprsubrg  15566  rhmpropd  15580  isabv  15584  issrngd  15626  islmod  15631  lmodprop2d  15687  islss  15692  islssd  15693  lssats2  15757  lspsnel  15760  islmhm  15784  lmhmf1o  15803  lmhmima  15804  lmhmpreima  15805  reslmhm  15809  lmhmpropd  15826  islbs  15829  lspprel  15847  lspfixed  15881  lspindp4  15890  lsppratlem3  15902  lbsacsbs  15909  lbsextlem1  15911  lbsextlem2  15912  lbsextlem3  15913  lbsextlem4  15914  lidlmcl  15969  divscrng  15992  islpidl  15998  lidldvgen  16007  mplsubglem  16179  mpllsslem  16180  mplmonmul  16208  mplrcl  16231  subrgascl  16239  subrgasclcl  16240  strov2rcl  16315  zrhrhmb  16465  znf1o  16505  frgpcyg  16527  isphld  16558  elocv  16568  iscss  16583  isobs  16620  obs2ss  16629  istopon  16663  eltg  16695  eltg2  16696  eltop  16712  eltop2  16713  eltop3  16714  pptbas  16745  iscld  16764  neiss2  16838  isnei  16840  lpfval  16870  lpval  16871  islp  16872  maxlp  16878  islpi  16880  restlp  16913  ordtbas2  16921  ordtrest2  16934  lmfval  16962  cnfval  16963  iscn  16965  iscnp  16967  tgcn  16982  tgcnp  16983  lmbrf  16990  cnpresti  17016  ist1  17049  ist1-2  17075  cnt1  17078  haust1  17080  cmpfi  17135  cmpfii  17136  1stcfb  17171  2ndc1stc  17177  1stcrest  17179  2ndcdisj  17182  1stcelcls  17187  nllyi  17201  subislly  17207  kgenval  17230  elkgen  17231  kgencn2  17252  txbas  17262  eltx  17263  ptval  17265  ptpjpre1  17266  ptopn2  17279  ptpjopn  17306  ptclsg  17309  xkoccn  17313  txdis  17326  txdis1cn  17329  ptrescn  17333  hausdiag  17339  hauseqlcld  17340  txhaus  17341  xkohaus  17347  elqtop  17388  qtopeu  17407  kqcldsat  17424  hmeofval  17449  ptuncnv  17498  ptunhmeo  17499  elmptrab  17522  fbdmn0  17529  elfg  17566  elfilss  17571  filunirn  17577  fixufil  17617  elfm  17642  rnelfmlem  17647  rnelfm  17648  fmfnfmlem4  17652  elflim2  17659  flimtopon  17665  elflim  17666  hausflim  17676  flimcls  17680  flfnei  17686  isflf  17688  hausflf  17692  cnpflf  17696  cnflf  17697  txflf  17701  isfcls  17704  fclstopon  17707  isfcls2  17708  fclssscls  17713  fclsnei  17714  fclsfnflim  17722  flimfnfcls  17723  isfcf  17729  fcfelbas  17731  cnpfcf  17736  cnfcf  17737  alexsublem  17738  alexsubALTlem3  17743  tmdgsum2  17779  tgpconcomp  17795  ghmcnp  17797  divstgplem  17803  eltsms  17815  haustsms  17818  tsmsgsum  17821  tsmssubm  17825  tsmssplit  17834  ismet  17888  isxmet  17889  elbl  17949  elmopn  17988  prdsbl  18037  neibl  18047  met1stc  18067  metrest  18070  prdsxmslem2  18075  txmetcnp  18093  txmetcn  18094  tngngp  18170  isnmhm  18255  zcld  18319  metnrmlem1a  18362  elcncf  18393  cncfcnvcn  18424  cnheibor  18453  lebnumlem1  18459  ishtpy  18470  isphtpy  18479  om1elbas  18530  elpi1  18543  pi1xfr  18553  pi1coghm  18559  tchcph  18667  lmmbrf  18688  iscfil  18691  iscau  18702  iscauf  18706  caucfil  18709  iscmet  18710  cmetcaulem  18714  iscmet3lem1  18717  iscmet3lem2  18718  iscmet3  18719  bcthlem1  18746  cmsss  18772  minveclem3b  18792  ovolfioo  18827  ovolficc  18828  ovolctb  18849  ovoliunnul  18866  ovolshftlem1  18868  sca2rab  18871  ovolscalem1  18872  ovolicc2lem1  18876  ovolicc2lem2  18877  ovolicc2lem4  18879  ovolicc2lem5  18880  iundisj  18905  iunmbl2  18914  uniioombllem3  18940  vitalilem2  18964  vitalilem3  18965  mbfss  19001  i1faddlem  19048  i1fmullem  19049  mbfi1fseqlem2  19071  mbfi1fseqlem4  19073  mbfi1fseq  19076  itg2splitlem  19103  itg2split  19104  itg2monolem1  19105  itg2gt0  19115  isibl  19120  iblss2  19160  itgss3  19169  itgsplit  19190  ellimc  19223  limcmo  19232  cnlimc  19238  limciun  19244  limcun  19245  eldv  19248  dvbsss  19252  dvreslem  19259  elcpn  19283  dvaddf  19291  dvmulf  19292  dvcof  19297  rolle  19337  dvlip2  19342  dvivthlem1  19355  lhop1  19361  lhop2  19362  ftc1cn  19390  mpfind  19428  fta1glem2  19552  plyco0  19574  elply  19577  ply1termlem  19585  eltayl  19739  tayl0  19741  taylplem1  19742  taylplem2  19743  dvtaylp  19749  taylthlem1  19752  taylthlem2  19753  abelth  19817  cxpcn3  20088  rlimcnp  20260  fsumharmonic  20305  dchrelbas  20475  pntrsumbnd2  20716  ostth2lem2  20783  ex-res  20828  isabloda  20966  issubgo  20970  isass  20983  elghomlem2  21029  ghablo  21036  iscom2  21079  rngoidmlem  21090  rngo1cl  21096  isssp  21300  sspn  21312  islno  21331  isblo  21360  nmlno0  21373  ishmo  21389  dipdir  21420  dipass  21423  ubthlem1  21449  ubthlem2  21450  htthlem  21497  htth  21498  ocel  21860  ocnel  21877  shsel  21893  shsel2  21901  shmodsi  21968  pjhtheu  21973  pjeq  21978  axpjpj  21999  pjoc2  22018  elspani  22122  h1de2ctlem  22134  elspansn  22145  elspansn2  22146  elnlfn  22508  eleigvec  22537  riesz3i  22642  ballotlemfc0  23051  ballotlemfcc  23052  ballotlemsima  23074  ballotlemrv  23078  eliccioo  23115  iuneq12daf  23154  iuneq12df  23155  iunrdx  23161  itgeq12dv  23196  elunirn2  23215  fmptdF  23221  fmptcof2  23229  funcnvmptOLD  23234  funcnvmpt  23235  xrofsup  23255  cnre2csqima  23295  cbvdisjf  23350  disjorf  23356  disjabrex  23359  disjabrexf  23360  iundisjfi  23363  iundisjf  23365  disjrdx  23370  xrge0tsmsbi  23383  ofcfval  23459  measvuni  23542  measiuns  23544  meascnbl  23546  ismbfm  23557  elunirnmbfm  23558  isanmbfm  23561  imambfm  23567  dya2iocrrnval  23582  probfinmeasb  23632  rrvmbfm  23645  elorvc  23660  elorrvc  23664  dstrvprob  23672  dstfrvel  23674  dstfrvunirn  23675  subfacp1lem2b  23712  subfacp1lem4  23714  subfacp1lem5  23715  subfacp1lem6  23716  ptpcon  23764  cvmscbv  23789  iscvm  23790  cvmsi  23796  cvmsval  23797  cvmliftmolem1  23812  cvmlift2lem12  23845  cvmlift2lem13  23846  cvmlift3lem7  23856  vdgrfval  23889  vdgrun  23893  vdgr1a  23897  eupap1  23900  eupath2lem3  23903  snmlval  23914  elgiso  24003  mpteq12d  24128  predbrg  24186  trpredrec  24241  wfrlem9  24264  wfrlem12  24267  fvnobday  24336  nodenselem3  24337  nodenselem5  24339  nofulllem5  24360  elee  24522  brbtwn  24527  brcgr  24528  axlowdimlem16  24585  funtransport  24654  fvtransport  24655  brcolinear  24682  colineardim1  24684  funray  24763  fvray  24764  funline  24765  fvline  24767  lineelsb2  24771  rankelg  24798  rankeq1o  24801  elhf2  24805  0hf  24807  domrngref  25060  repfuntw  25160  repcpwti  25161  dstr  25171  iscst3  25176  islatalg  25183  valcurfn1  25204  isorhom  25211  isoriso2  25213  puub2  25258  puub  25259  mxlelt  25264  ismxl2  25267  ismnl2  25268  isdir2  25292  prodeq2  25307  prodeq3ii  25308  dffprod  25319  iscom  25333  clfsebsr  25349  imtr  25398  prsubrtr  25399  isfldOLD  25426  idlvalNEW  25445  isidlNEW  25446  basexre  25522  nsn  25530  intopcoaconb  25540  usptoplem  25546  istopx  25547  usptop  25550  prcnt  25551  filint2  25553  conttnf2  25562  limptlimpr2lem1  25574  limptlimpr2lem2  25575  altretop  25600  iintlem1  25610  supnuf  25629  cnegvex2b  25662  rnegvex2b  25663  isded  25736  dedi  25737  iscatOLD  25754  cati  25755  dualded  25783  dualcat2  25784  ishomc  25789  ishomd  25790  ismonb  25810  imonclem  25813  isepib  25820  iepiclem  25823  isfuna  25834  isfunb  25835  issubcata  25846  idsubfun  25858  isinob  25862  issrc  25867  propsrc  25868  isntr  25873  islimcat  25876  vtarsuelt  25895  prismorcset  25914  prismorcset2  25918  domcatfun  25925  codcatfun  25934  prismorcset3  25938  isrocatset  25957  cmppar3  25974  setiscat  25979  isnword  25986  1iskle  25989  indcls2  25996  empklst  26009  clscnc  26010  phckle  26027  psckle  26028  fnckle  26045  cndpv  26049  pgapspf  26052  pgapspf2  26053  lineval22  26082  lineval2a  26085  lineval2b  26086  lineval5a  26088  lineval6a  26089  iscol2  26093  isconcl2b  26098  isibg2  26110  isibg2aa  26112  isibg2aalem1  26113  isibg2aalem2  26114  sgplpte21  26132  sgplpte22  26138  sgplpte21d1  26139  sgplpte21d2  26140  lppotoslem  26143  isray2  26153  isray  26154  isside0  26164  abhp  26173  abhp1  26174  isibcg  26191  islocfin  26296  lfinpfin  26303  locfindis  26305  locfincf  26306  comppfsc  26307  neibastop2lem  26309  neibastop3  26311  eltail  26323  indexdom  26413  incsequz  26458  istotbnd  26493  istotbnd3  26495  0totbnd  26497  sstotbnd  26499  sstotbnd3  26500  isbnd  26504  prdstotbnd  26518  cntotbnd  26520  isismty  26525  heibor1lem  26533  heiborlem2  26536  heiborlem3  26537  heibor  26545  exidcl  26566  exidreslem  26567  divrngcl  26588  isdrngo2  26589  isrngohom  26596  isrngoiso  26609  isriscg  26615  iscringd  26624  isidl  26639  ispridl  26659  ismaxidl  26665  prter3  26750  fnelfp  26755  fnelnfp  26757  isnacs  26779  mrefg2  26782  elmzpcl  26804  mzpcompact2  26830  eldiophb  26836  elpell1qr  26932  elpell14qr  26934  elpell1234qr  26936  pw2f1ocnv  27130  pw2f1o2val2  27133  aomclem4  27154  aomclem6  27156  islssfg2  27169  pwssplit3  27190  dsmmbas2  27203  dsmmfi  27204  dsmmelbas  27205  dsmmlss  27210  frlmelbas  27224  frlmlbs  27249  frlmup1  27250  ellspd  27254  imasgim  27264  islinds  27279  islindf2  27284  f1lindf  27292  islindf4  27308  lnr2i  27320  elmnc  27341  rngunsnply  27378  f1otrspeq  27390  pmtrfrn  27400  psgnunilem1  27416  psgnunilem5  27417  psgnunilem2  27418  psgnunilem3  27419  psgneldm2  27427  mat1  27482  issdrg  27505  dvconstbi  27551  fnchoice  27700  rfcnpre3  27704  rfcnpre4  27705  fmul01lt1lem2  27715  stoweidlem11  27760  stoweidlem26  27775  stoweidlem27  27776  stoweidlem29  27778  stoweidlem31  27780  stoweidlem34  27783  stoweidlem48  27797  stoweidlem57  27806  stoweidlem59  27808  afvelrnb  28025  afvelrnb0  28026  mpt2xopn0yelv  28079  mpt2xopovel  28086  nbgraop  28140  nbgrael  28141  nbusgra  28143  nbgraeledg  28145  iscusgra  28153  isuvtx  28160  uvtxel  28161  uvtxisvtx  28162  bnj945  28805  bnj1400  28868  bnj18eq1  28959  bnj916  28965  bnj1014  28992  bnj1015  28993  bnj1110  29012  bnj1417  29071  islshp  29169  islsat  29181  lcvfbr  29210  islfl  29250  ellkr  29279  islshpkrN  29310  ldual1dim  29356  isopos  29370  cmtfvalN  29400  cvrfval  29458  isat  29476  islln  29695  islpln  29719  islvol  29762  isline  29928  ispointN  29931  ispsubsp  29934  elpmap  29947  elpmapat  29953  elpadd  29988  paddclN  30031  elpclN  30081  elpcliN  30082  pclfinN  30089  pclcmpatN  30090  ispsubclN  30126  iswatN  30183  islhp  30185  islaut  30272  ispautN  30288  isldil  30299  isltrn  30308  isdilN  30343  istrnN  30346  istendo  30949  dvhb1dimN  31175  erng1lem  31176  erngdvlem4-rN  31188  diaelval  31223  diaeldm  31226  dia1dimid  31253  cdlemm10N  31308  dibopelvalN  31333  dibopelval2  31335  dibelval3  31337  dibelval1st  31339  dibelval2nd  31342  dibeldmN  31348  dibvalrel  31353  dibglbN  31356  dicffval  31364  dicfval  31365  dicopelval  31367  dicelvalN  31368  dicelval3  31370  dicvalrelN  31375  dicelval1sta  31377  diclspsn  31384  dihopelvalbN  31428  dihopelvalcqat  31436  dihopelvalcpre  31438  dihvalrel  31469  dih1  31476  dihmeetlem4preN  31496  dihmeetlem13N  31509  dih1dimatlem  31519  dochnel2  31582  dochnel  31583  dihjatcclem4  31611  dvh2dim  31635  dvh3dim  31636  dvh4dimN  31637  dochfln0  31667  lpolsetN  31672  islpolN  31673  lcfrvalsnN  31731  lcfrlem21  31753  lcfrlem27  31759  lcfrlem37  31769  lcfr  31775  lcdlss  31809  mapdcv  31850  mapdindp2  31911  mapdindp4  31913  mapdh6dN  31929  hdmap1fval  31987  hdmap1l6d  32004  hdmapffval  32019  hdmapfval  32020  hdmapval  32021  hgmapffval  32078  hgmapfval  32079  hdmapellkr  32107  hlhilhillem  32153
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-cleq 2276  df-clel 2279
  Copyright terms: Public domain W3C validator