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

Theorem feq2d 5700
Description: Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypothesis
Ref Expression
feq2d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
feq2d  |-  ( ph  ->  ( F : A --> C 
<->  F : B --> C ) )

Proof of Theorem feq2d
StepHypRef Expression
1 feq2d.1 . 2  |-  ( ph  ->  A  =  B )
2 feq2 5696 . 2  |-  ( A  =  B  ->  ( F : A --> C  <->  F : B
--> C ) )
31, 2syl 16 1  |-  ( ph  ->  ( F : A --> C 
<->  F : B --> C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1398   -->wf 5566
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-cleq 2446  df-fn 5573  df-f 5574
This theorem is referenced by:  feq12d  5702  ffdm  5727  fsng  6046  fsnunf2  6086  issmo2  7012  qliftf  7391  elpm2r  7429  ralxpmap  7461  ordtypelem5  7939  axdc3lem3  8823  axdc3lem4  8824  fseq1p1m1  11756  fseq1m1p1  11757  seqf1o  12130  iswrdi  12537  wrdf  12538  snopiswrd  12543  ffz0iswrd  12556  wrdnval  12559  swrdf  12641  swrd0f  12643  cats1un  12692  cshwf  12762  wrdlen2i  12875  wrd2pr2op  12876  wwlktovf  12885  rlimi  13418  rlimmptrcl  13512  lo1mptrcl  13526  o1mptrcl  13527  o1fsum  13709  ram0  14624  funcres  15384  curf2cl  15699  uncfcurf  15707  yonedalem4c  15745  intopsn  16081  gsumprval  16107  resmhm  16189  gsumwsubmcl  16205  gsumccat  16208  gsumwmhm  16212  frmdup1  16231  frmdup3lem  16233  isghm  16466  resghm  16482  subgga  16537  gasubg  16539  psgnunilem2  16719  sylow2blem2  16840  pj2f  16915  pj1ghm  16920  frgpupf  16990  frgpup3lem  16994  gsumval3OLD  17107  gsumval3  17110  gsummptfzcl  17192  dprdf2  17235  ablfaclem2  17332  ablfac2  17335  isabvd  17664  abvpropd  17686  mplasclf  18357  evlssca  18386  lply1binomsc  18544  cygznlem2a  18779  frgpcyg  18785  mat1dimelbas  19140  mat2pmatbas  19394  cpmadugsumlemF  19544  cnpf2  19918  lmcnp  19972  ptpjcn  20278  pt1hmeo  20473  cnextfres  20734  cnmpt2pc  21594  pi1addf  21713  pi1xfrf  21719  pi1cof  21725  mbfmptcl  22210  iblcnlem  22361  limcres  22456  cnplimc  22457  limccnp  22461  limccnp2  22462  limcun  22465  dvidlem  22485  cpnord  22504  dvaddf  22511  dvmulf  22512  dvcmulf  22514  dvcof  22517  dvcj  22519  dvrec  22524  dvmptcl  22528  dvcnvlem  22543  dvcnv  22544  rolle  22557  cmvth  22558  mvth  22559  dvlip  22560  dvlipcn  22561  c1lip2  22565  dv11cn  22568  dvivthlem1  22575  dvivthlem2  22576  dvivth  22577  dvne0  22578  lhop1lem  22580  lhop1  22581  lhop2  22582  lhop  22583  dvcnvrelem2  22585  taylthlem1  22934  taylthlem2  22935  ulmf2  22945  ulm2  22946  ulmdv  22964  pserdv  22990  rlimcxp  23501  o1cxp  23502  dchrptlem2  23738  axlowdimlem5  24451  axlowdimlem7  24453  axlowdimlem10  24456  uhgraun  24513  wrdumgra  24518  umgraf  24520  umgra1  24528  umgraun  24530  wlkelwrd  24732  2trllemH  24756  2trllemG  24762  is2wlk  24769  redwlk  24810  usgra2adedgwlkonALT  24818  usgra2wlkspthlem1  24821  usgra2wlkspthlem2  24822  fargshiftf  24838  3v3e3cycl1  24846  4cycl4v4e  24868  4cycl4dv  24869  4cycl4dv4e  24870  wlkiswwlk2lem3  24895  wlkiswwlk2  24899  vfwlkniswwlkn  24908  clwlkisclwwlklem2a  24987  clwlkisclwwlklem2  24988  clwlkfclwwlk2wrd  25042  clwlkf1clwwlklem3  25050  el2wlkonotlem  25064  eupai  25169  eupatrl  25170  eupa0  25176  eupares  25177  eupap1  25178  isgrpo  25396  elghomlem1OLD  25561  rngosn3  25626  vci  25639  isvclem  25668  vcoprnelem  25669  isnvlem  25701  ajfval  25922  acunirnmpt2  27727  acunirnmpt2f  27728  locfinref  28079  1stmbfm  28468  2ndmbfm  28469  sibfof  28546  rrvf2  28651  signshf  28809  cvmliftmolem1  28990  cvmliftlem7  29000  cvmliftlem10  29003  cvmlift2lem9  29020  filnetlem4  30439  sdclem2  30475  sdclem1  30476  sdc  30477  fdc  30478  sstotbnd2  30510  mptelpm  31693  cncfuni  31928  cncfiooicclem1  31935  dvsubf  31948  dvdivf  31958  dvbdfbdioolem1  31964  ioodvbdlimc1lem1  31967  ioodvbdlimc1lem2  31968  ioodvbdlimc1  31969  ioodvbdlimc2lem  31970  ioodvbdlimc2  31971  dvnprodlem3  31984  itgsubsticclem  32013  fourierdlem48  32176  fourierdlem49  32177  fourierdlem58  32186  fourierdlem59  32187  fourierdlem60  32188  fourierdlem61  32189  fourierdlem69  32197  fourierdlem75  32203  fourierdlem81  32209  fourierdlem89  32217  fourierdlem91  32219  fourierdlem97  32225  fourierdlem113  32241  2ffzoeq  32715  usgra2pthspth  32723  usgra2pthlem1  32725  usgra2pth  32726  uhgun  32752  resmgmhm  32858  elbigolo1  33432
  Copyright terms: Public domain W3C validator