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

Theorem eqeq12d 2418
Description: A useful inference for substituting definitions into an equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
eqeq12d.1  |-  ( ph  ->  A  =  B )
eqeq12d.2  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
eqeq12d  |-  ( ph  ->  ( A  =  C  <-> 
B  =  D ) )

Proof of Theorem eqeq12d
StepHypRef Expression
1 eqeq12d.1 . 2  |-  ( ph  ->  A  =  B )
2 eqeq12d.2 . 2  |-  ( ph  ->  C  =  D )
3 eqeq12 2416 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  =  C  <-> 
B  =  D ) )
41, 2, 3syl2anc 643 1  |-  ( ph  ->  ( A  =  C  <-> 
B  =  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649
This theorem is referenced by:  cdeqeq  3116  sbceqg  3227  csbing  3508  csbifg  3727  uniprg  3990  unisng  3992  intprg  4044  iununi  4135  csbopabg  4243  limeq  4553  ordunisuc  4771  onsucuni2  4773  orduninsuc  4782  csbima12g  5172  dmsnsnsn  5307  cnvsng  5314  csbiotag  5406  csbfv12gALT  5698  fveqres  5723  fvmptf  5780  eqfnfv2f  5790  fvreseq  5792  fmptco  5860  fnressn  5877  fvsng  5886  fnpr  5909  fnprOLD  5910  fnsuppres  5911  cocan1  5983  cocan2  5984  fliftfun  5993  weniso  6034  csbovg  6071  eqfnov  6135  ovmpt2s  6156  ov2gf  6157  ovmpt2dxf  6158  caovcomg  6201  caovassg  6204  caovcang  6207  caovcanrd  6209  caovcan  6210  caovdig  6220  caovdirg  6223  caovmo  6243  grprinvlem  6244  grprinvd  6245  offveqb  6285  caofid0l  6291  caofid0r  6292  caofass  6297  caonncan  6301  op1stg  6318  op2ndg  6319  f1o2ndf1  6413  opabiota  6497  csbriotag  6521  onfununi  6562  tfrlem1  6595  tfrlem2  6596  tfrlem3  6597  tfrlem3a  6598  tfrlem9  6605  tfrlem11  6608  tfrlem12  6609  tfr3  6619  tz7.44-1  6623  tz7.44-2  6624  tz7.44-3  6625  rdglem1  6632  rdg0g  6644  seqomlem1  6666  abianfp  6675  oalim  6735  omlim  6736  oelim  6737  oa0r  6741  om0r  6742  om1r  6745  oaass  6763  oarec  6764  odi  6781  omass  6782  oelim2  6797  oeoalem  6798  oeoa  6799  oeoelem  6800  oeoe  6801  nna0r  6811  nnacom  6819  nnaass  6824  nndi  6825  nnmass  6826  nnmsucr  6827  nnmcom  6828  oaabs  6846  oaabs2  6847  omabs  6849  ecovcom  6974  ecovass  6975  ecovdi  6976  dom2lem  7106  unxpdomlem2  7273  unxpdomlem3  7274  ixpfi2  7363  fipreima  7370  ordiso2  7440  wemaplem1  7471  wemaplem2  7472  wemapso2lem  7475  cantnfval2  7580  cantnfp1lem3  7592  oemapvali  7596  cantnflem1c  7599  cantnflem1  7601  wemapwe  7610  tcvalg  7633  rankvalg  7699  rankonidlem  7710  ranklim  7726  rankuni  7745  cardprclem  7822  cardprc  7823  carduni  7824  fseqenlem1  7861  fodomacn  7893  alephcard  7907  alephfp2  7946  alephval3  7947  dfac12lem1  7979  dfac12lem2  7980  dfac12r  7982  ackbij1lem5  8060  ackbij1lem8  8063  ackbij1lem14  8069  ackbij1lem16  8071  ackbij2lem3  8077  cardcf  8088  sornom  8113  fin23lem28  8176  isf32lem2  8190  itunitc  8257  ituniiun  8258  axdc3lem2  8287  axdc4lem  8291  ttukeylem3  8347  ttukey2g  8352  fpwwe2lem8  8468  fpwwecbv  8475  canth4  8478  pwfseqlem2  8490  addcanpi  8732  mulcanpi  8733  recrecnq  8800  ltexnq  8808  genpv  8832  0idsr  8928  1idsr  8929  ax1rid  8992  mulid1  9044  addcan  9206  addcan2  9207  mulcand  9611  mulcan2d  9612  div11  9660  divmuleq  9675  conjmul  9687  eqneg  9690  ofsubeq0  9953  rpnnen1  10561  cnref1o  10563  xmulasslem  10820  xmulass  10822  xadddi2  10832  prunioo  10981  fzsuc2  11060  fzprval  11062  fztpval  11063  modadd1  11233  modmul1  11234  om2uzsuci  11243  om2uzrdg  11251  uzrdgxfr  11261  seq1  11291  seqp1  11293  seqfveq2  11300  seqfveq  11302  seqshft2  11304  seqsplit  11311  seqcaopr3  11313  seqcaopr2  11314  seqf1olem2a  11316  seqf1olem2  11318  seqf1o  11319  seqid  11323  seqid2  11324  seqhomo  11325  ser1const  11334  seqof2  11336  mulexp  11374  expadd  11377  expmul  11380  binom2  11451  sq01  11456  modexp  11469  bcpasc  11567  hashgadd  11606  hashdom  11608  hashfzo  11649  hashxplem  11651  hashxp  11652  hashmap  11653  hashpw  11654  hashbclem  11656  hashbc  11657  hashfacen  11658  hashf1lem1  11659  hashf1lem2  11660  hashf1  11661  seqcoll  11667  ccatopth  11731  ccatopth2  11732  cats1un  11745  replim  11876  cjreb  11883  cjexp  11910  absexp  12064  abs1m  12094  recan  12095  isercoll2  12417  iseraltlem2  12431  iseraltlem3  12432  sumeq2w  12441  sumeq2ii  12442  zsum  12467  fsum  12469  fsumf1o  12472  sumss  12473  fsumcvg2  12476  fsumadd  12487  isummulc2  12501  fsum2d  12510  fsummulc2  12522  fsumconst  12528  fsumparts  12540  fsumrelem  12541  fsumiun  12555  binom  12564  bcxmas  12570  incexclem  12571  isumshft  12574  isumnn0nn  12577  climcndslem1  12584  climcndslem2  12585  mertenslem2  12617  efne0  12653  efexp  12657  demoivreALT  12757  moddvds  12814  bitsinv1  12909  sadadd2  12927  smu01lem  12952  smupval  12955  smueqlem  12957  smumullem  12959  gcdaddm  12984  bezoutlem1  12993  bezout  12997  gcddiv  13004  seq1st  13017  alginv  13021  algfx  13026  isprm2lem  13041  nn0gcdsq  13099  crt  13122  eulerthlem2  13126  pythagtriplem1  13145  iserodd  13164  pcqmul  13182  pcexp  13188  pcneg  13202  pcmpt  13216  pcfac  13223  prmreclem2  13240  prmreclem3  13241  1arith  13250  vdwpc  13303  ramcl  13352  imasval  13692  ercpbllem  13728  xpscfv  13742  iscat  13852  iscatd  13853  catideu  13855  iscatd2  13861  catlid  13863  catrid  13864  catass  13866  proplem  13870  homfeq  13875  comfeq  13887  catpropd  13890  moni  13917  epii  13924  sectffval  13931  sectfval  13932  oppcsect  13954  sectmon  13958  isfunc  14016  funcid  14022  funcco  14023  funcpropd  14052  isfull  14062  fthsect  14077  fthmon  14079  natfval  14098  isnat  14099  nati  14107  fucsect  14124  natpropd  14128  setcmon  14197  setcepi  14198  setcsect  14199  evlfcl  14274  uncfcurf  14291  yoniso  14337  isacs5lem  14550  acsdrscl  14551  acsficl  14552  latdisdlem  14570  latdisd  14571  isdlat  14574  dlatmjdi  14575  isps  14589  ismnd  14647  mgmidmo  14648  mndlem1  14649  mgmlrid  14667  ismndd  14674  mndpropd  14676  imasmnd2  14687  ismhm  14695  mhmpropd  14699  mhmlin  14700  mhmeql  14719  gsumvalx  14729  gsumval2  14738  gsumccat  14742  gsumwmhm  14745  frmdgsum  14762  isgrp  14771  grppropd  14778  isgrpd2e  14782  isgrpid2  14796  grpidd2  14797  grpinvfval  14798  grpinvpropd  14821  grpsubrcan  14825  grplactcnv  14842  mulgnn0p1  14856  mulgneg2  14872  mulgnnass  14873  mulgnn0ass  14874  mulgass  14875  mhmmulg  14877  imasgrp2  14888  isghm  14961  ghmlin  14966  ghmeql  14983  isga  15023  gagrpid  15026  gaass  15029  galcan  15036  orbsta  15045  cayleylem2  15066  cntzfval  15074  elcntz  15076  cntzsnval  15078  elcntzsn  15079  cntzi  15083  resscntz  15085  cntzmhm  15092  gsumwrev  15117  odfval  15126  mndodcong  15135  odbezout  15149  odeq1  15151  submod  15158  gexval  15167  gexdvds  15173  ispgp  15181  sylow1lem1  15187  sylow2alem1  15206  sylow2alem2  15207  sylow2blem2  15210  efgmnvl  15301  efgredlemc  15332  efgredeu  15339  frgpuptinv  15358  frgpup1  15362  frgpup3lem  15364  iscmn  15374  cmnpropd  15376  iscmnd  15379  abladdsub4  15393  submcmn2  15413  divsabl  15435  iscyg  15444  cygabl  15455  gsum2d  15501  dmdprd  15514  dprdval  15516  dprdfcntz  15528  subgdmdprd  15547  dprd2da  15555  dpjrid  15575  pgpfac1lem3a  15589  ablfaclem3  15600  ablfac2  15602  isrng  15623  rngpropd  15650  mulgass2  15665  imasrng  15680  dvdsr  15706  dvreq1  15753  isdrng  15794  drngprop  15801  isdrngd  15815  drngpropd  15817  isabv  15862  abvmul  15872  issrng  15893  issrngd  15904  islmod  15909  lmodlema  15910  islmodd  15911  lmodprop2d  15961  islmhm  16058  lmhmlin  16066  islmhm2  16069  lmhmeql  16086  lmhmpropd  16100  islbs  16103  lbspropd  16126  divscrng  16266  islpir  16275  rrgval  16302  unitrrg  16308  isassa  16330  assalem  16331  isassad  16337  assapropd  16341  mvrf1  16444  mplmonmul  16482  mplcoe1  16483  mplcoe3  16484  mplcoe2  16485  coe1tm  16620  ply1sclf1  16635  cnfldmulg  16688  cnfldexp  16689  prmirredlem  16728  chrcong  16765  zndvds  16785  znf1o  16787  znunit  16799  cygznlem3  16805  frgpcyg  16809  isphl  16814  ipcj  16820  iporthcom  16821  ip2eq  16839  isphld  16840  phlpropd  16841  ocvfval  16848  iscss  16865  ishil  16900  isobs  16902  obsip  16903  obslbs  16912  isperf  17169  restperf  17202  cmpsub  17417  iscon  17429  2ndcsep  17475  elptr2  17559  ptbasin  17562  dfac14  17603  txcnp  17605  ptcnplem  17606  ptcnp  17607  cnmpt11  17648  cnmpt21  17656  cnmptcom  17663  kqfeq  17709  isr0  17722  pt1hmeo  17791  ustexsym  18198  isusp  18244  imasdsf1olem  18356  isxms  18430  xmspropd  18456  imasf1oxms  18472  stdbdmopn  18501  isngp3  18598  ngppropd  18631  isnlm  18664  nmvs  18665  xrsxmet  18793  cnheibor  18933  htpyi  18952  htpycc  18958  pi1xfr  19033  pi1coghm  19039  isclm  19042  lmhmclm  19064  clmmulg  19071  iscph  19086  tchcph  19147  cmetcaulem  19194  bcth3  19237  ovolunlem1a  19345  ovolicc2lem1  19366  ovolicc2lem4  19369  ovolicc2  19371  mblsplit  19381  volun  19392  volfiniun  19394  voliunlem1  19397  volsup  19403  ioorinv  19421  uniioombllem2  19428  vitalilem3  19455  mbfeqalem  19487  mbflim  19513  itgeqa  19658  itgconst  19663  itgfsum  19671  itgsplitioo  19682  dvnadd  19768  dvnres  19770  dvexp  19792  dvmptfsum  19812  mvth  19829  dvlip  19830  lhop1lem  19850  dvcvx  19857  evlslem1  19889  mpfrcl  19892  evlsval  19893  mdegle0  19953  ply1nzb  19998  mon1pval  20017  facth1  20040  ig1pval  20048  dgrmulc  20142  dgrcolem1  20144  dgrcolem2  20145  dgrco  20146  coecj  20149  vieta1lem2  20181  vieta1  20182  elqaalem3  20191  dvntaylp  20240  ulmss  20266  mtest  20273  sineq0  20382  efif1olem4  20400  cxpexp  20512  mulcxplem  20528  mulcxp  20529  cxpmul2  20533  cxpeq  20594  affineequiv2  20621  quad2  20632  dcubic  20639  leibpi  20735  o1cxp  20766  scvxcvx  20777  wilthlem1  20804  wilthlem2  20805  perfect  20968  dchrelbas2  20974  dchrinv  20998  dchrptlem2  21002  lgsne0  21070  lgsqrlem2  21079  lgsdchr  21085  lgseisenlem2  21087  lgsquad2lem2  21096  dchrisumlem1  21136  qabvexp  21273  ostthlem1  21274  ostthlem2  21275  ostth3  21285  usgraidx2v  21365  nbgraf1olem5  21408  cusgrasize  21440  wlkntrllem2  21513  2wlklem  21517  constr1trl  21541  redwlk  21559  wlkdvspthlem  21560  iscrct  21564  iscycl  21565  fargshiftf1  21577  fargshiftfva  21579  usgrcyclnl2  21581  3v3e3cycl1  21584  constr3trllem5  21594  4cycl4v4e  21606  4cycl4dv4e  21608  iseupa  21640  eupatrl  21643  eupaseg  21648  eupap1  21651  eupath2  21655  isgrpo  21737  grpoass  21744  grpoidinvlem3  21747  grpoidinv  21749  grpoideu  21750  grpoidinv2  21759  grpoinvfval  21765  isgrp2d  21776  gxcom  21810  gxinv  21811  gxnn0add  21815  gxnn0mul  21818  isablo  21824  ablocom  21826  gxdi  21837  issubgoilem  21850  isass  21857  opidon  21863  exidu1  21867  cmpidelt  21870  elghomlem2  21903  ghomlin  21905  ghgrplem2  21908  ghgrp  21909  ghablo  21910  isrngo  21919  rngoid  21924  rngoideu  21925  rngodi  21926  rngodir  21927  rngoass  21928  iscom2  21953  vci  21980  vcid  21983  vcdi  21984  vcdir  21985  vcass  21986  isvclem  22009  isnvlem  22042  nvmeq0  22098  nvs  22104  imsmetlem  22135  islno  22207  lnolin  22208  ishmo  22265  isphg  22271  phpar2  22277  phpar  22278  ipdiri  22284  ipasslem1  22285  ipasslem5  22289  ipasslem11  22294  ipassi  22295  dipdir  22296  dipass  22299  ip2eqi  22311  htth  22374  hvsubsub4  22515  hvnegdi  22522  hvaddcan  22525  hvaddcan2  22526  hvsubcan  22529  hvsubcan2  22530  hvaddsub4  22533  hial2eq  22561  normlem9at  22576  normsq  22589  norm-iii  22595  normsub  22598  normpyth  22600  normpar  22610  polid  22614  ococ  22861  chj0  22952  chlejb1  22967  chdmm1  22980  chjass  22988  spanun  23000  spansn  23014  elspansn2  23022  cmbr  23039  cmbr3  23063  pjoml2  23066  pjoml3  23067  osum  23100  spansnj  23102  pjch1  23125  pjadji  23140  pjaddi  23141  pjinormi  23142  pjsubi  23143  pjmuli  23144  pjcjt2  23147  pjch  23149  pjopyth  23175  pjpyth  23180  hoaddcom  23230  hoaddass  23238  hocsubdir  23241  hoaddid1  23247  ho0sub  23253  honegsub  23255  adjsym  23289  eigrei  23290  eigre  23291  eigposi  23292  eigorth  23294  ellnop  23314  elhmop  23329  ellnfn  23339  cnvadj  23348  lnopl  23370  unop  23371  hmop  23378  lnfnl  23387  adj1  23389  eleigvec  23413  hoddi  23446  lnopeq0lem2  23462  lnopunilem1  23466  lnopunilem2  23467  lnopunii  23468  elunop2  23469  lnophmi  23474  lnfnmul  23504  cnlnadjlem5  23527  branmfn  23561  bra11  23564  hmopidmchi  23607  hmopidmch  23609  hmopidmpj  23610  pjss2coi  23620  pjssmi  23621  pjssge0i  23622  pjidmco  23637  dfpjop  23638  elpjrn  23646  isst  23669  ishst  23670  hstel2  23675  stj  23691  mdbr  23750  mdi  23751  mdbr3  23753  dmdbr  23755  dmdmd  23756  dmdi  23758  dmdbr3  23761  mddmd2  23765  mdsl1i  23777  chjatom  23813  iuninc  23964  fmptcof2  24029  bcm1n  24104  xmulcand  24120  xrsmulgzz  24153  pstmxmet  24245  cnre2csqlem  24261  mndpluscn  24265  qqhval2  24319  esumfzf  24412  esumcvg  24429  ofcfeqd2  24437  ismeas  24506  isrnmeas  24507  measvun  24516  probun  24630  facgam  24803  subfacp1lem3  24821  subfacp1lem4  24822  subfacp1lem5  24823  subfacp1lem6  24824  subfacval2  24826  erdszelem9  24838  sconpht  24869  ptpcon  24873  cvmliftmolem1  24921  cvmliftmolem2  24922  cvmliftlem10  24934  cvmlift2  24956  cvmliftphtlem  24957  ghomgrpilem1  25049  relexpsucr  25083  relexpsucl  25085  relexpcnv  25086  relexpadd  25091  sqdivzi  25137  mulcan2g  25143  shftvalg  25161  clim2prod  25169  prodfrec  25176  prodeq2w  25191  prodeq2ii  25192  zprod  25216  fprod  25220  fprodf1o  25225  fprodser  25228  fprodmul  25237  fproddiv  25238  prodsn  25239  fprodabs  25250  fprodefsum  25251  fprodconst  25255  fprod2d  25258  iprodefisumlem  25270  binomfallfac  25308  faclimlem1  25310  fprb  25343  rdgprc  25365  dfrdg2  25366  preddowncl  25410  poseq  25467  soseq  25468  wfr3g  25469  wfrlem1  25470  wfrlem12  25481  wfrlem14  25483  wfrlem15  25484  wfr2  25487  wfr2c  25488  tfr3ALT  25493  frr3g  25494  frrlem1  25495  frrlem11  25507  sltval2  25524  sltres  25532  nofulllem5  25574  fvsingle  25673  fullfunfv  25700  brcgr  25743  brbtwn2  25748  colinearalglem1  25749  colinearalg  25753  ax5seglem1  25771  ax5seglem2  25772  ax5seglem8  25779  ax5seglem9  25780  axlowdimlem13  25797  axlowdimlem16  25800  axlowdim1  25802  axcontlem1  25807  axcontlem2  25808  axcontlem6  25812  axcontlem7  25813  axcontlem8  25814  lineelsb2  25986  bpolyval  25999  bpolydif  26005  rankung  26011  ranksng  26012  rankpwg  26014  voliunnfl  26149  volsupnfl  26150  opnregcld  26223  cldregopn  26224  neibastop3  26281  cocanfo  26309  upixp  26321  sdclem2  26336  caushft  26357  ismtycnv  26401  ismtyima  26402  ismtybndlem  26405  ismtyres  26407  bfplem2  26422  bfp  26423  grpoeqdivid  26446  ghomco  26448  rngohomval  26470  isrngohom  26471  rngohomadd  26475  rngohommul  26476  iscringd  26499  crngocom  26501  crngohomfo  26506  dmncan2  26577  fnelfp  26626  ismrcd2  26643  ismrc  26645  dvdsrabdioph  26760  fphpdo  26768  rmxypairf1o  26864  monotoddzzfi  26895  monotoddzz  26896  oddcomabszz  26897  rmxdioph  26977  expdiophlem2  26983  dnnumch3  27012  aomclem8  27027  islssfg  27036  unxpwdom3  27124  gicabl  27131  pmtrfrn  27268  cntzsdrg  27378  idomodle  27380  fgraphxp  27398  hausgraph  27399  caofcan  27408  expgrowth  27420  fmuldfeq  27580  climmulf  27597  climexp  27598  climsuse  27601  climrecf  27602  stoweidlem30  27646  stoweidlem48  27664  wallispilem4  27684  wallispi2lem1  27687  wallispi2lem2  27688  csbafv12g  27868  csbaovg  27911  swrdccatin1  28016  swrdccatin12c  28028  swrdccat3b  28031  usgra2pthspth  28035  usgra2wlkspthlem1  28036  usgra2pthlem1  28040  usgra2pth  28041  2pthfrgra  28115  bnj1385  28910  bnj66  28937  bnj106  28945  bnj155  28956  bnj222  28960  bnj540  28969  bnj591  28988  bnj594  28989  bnj611  28995  bnj893  29005  bnj1000  29018  bnj966  29021  bnj1112  29058  bnj1234  29088  bnj1253  29092  bnj1280  29095  bnj1326  29101  bnj1450  29125  bnj1463  29130  bnj1529  29145  lshpset  29461  lcvexchlem4  29520  lcvexchlem5  29521  lflset  29542  islfl  29543  lfli  29544  islfld  29545  eqlkr3  29584  isopos  29663  oposlem  29666  opcon3b  29679  cmtvalN  29694  omllaw  29726  cvlexchb2  29814  cvlatexchb2  29818  cvlsupr2  29826  4atlem9  30085  4atlem10a  30086  4atlem11a  30089  4atlem12a  30092  4at2  30096  pmapglb2N  30253  pmapglb2xN  30254  paddasslem17  30318  ispsubclN  30419  ispsubcl2N  30429  lhpmod2i2  30520  lhpmod6i1  30521  4atexlemex2  30553  4atex  30558  4atex2-0aOLDN  30560  4atex2-0cOLDN  30562  ldilval  30595  ltrnfset  30599  ltrnset  30600  isltrn  30601  ltrneq2  30630  trnfsetN  30637  trnsetN  30638  istrnN  30639  cdlemd5  30684  cdleme0moN  30707  cdleme0nex  30772  cdleme18d  30777  cdleme31so  30861  cdleme31fv  30872  cdlemg2jlemOLDN  31075  cdlemg2fvlem  31076  cdlemg2klem  31077  istendo  31242  tendovalco  31247  tendoeq2  31256  dicelvalN  31661  dihval  31715  dihcnv11  31758  dihmeetlem13N  31802  dihlspsnat  31816  dochn0nv  31858  dochkrshp4  31872  lpolsetN  31965  lpolsatN  31971  lpolpolsatN  31972  lcfl1lem  31974  lclkrlem2a  31990  lclkrlem2e  31994  lcfls1lem  32017  lclkrs2  32023  lcdfval  32071  lcdval  32072  mapdffval  32109  mapdfval  32110  mapd0  32148  mapdpglem30  32185  mapdhval  32207  mapdheq2  32212  hdmap1vallem  32281  hdmap1val  32282  hdmap1cbv  32286  hdmapval3N  32324  hdmap10  32326  hdmapeq0  32330  hdmap14lem12  32365  hdmap14lem13  32366  hgmapfval  32372  hgmapvs  32377  hgmapvv  32412  hlhilocv  32443
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
  Copyright terms: Public domain W3C validator