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

Theorem feq2d 5716
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 5712 . 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 1379   -->wf 5582
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2459  df-fn 5589  df-f 5590
This theorem is referenced by:  feq12d  5718  ffdm  5743  fsng  6058  fsnunf2  6098  issmo2  7017  qliftf  7396  elpm2r  7433  ralxpmap  7465  ordtypelem5  7943  axdc3lem3  8828  axdc3lem4  8829  fseq1p1m1  11748  fseq1m1p1  11749  seqf1o  12112  iswrdi  12514  wrdf  12515  snopiswrd  12518  ffz0iswrd  12530  wrdnval  12533  eqs1  12580  swrdf  12612  cats1un  12660  cshwf  12730  wrdlen2i  12843  wrd2pr2op  12844  wwlktovf  12853  rlimi  13295  rlimmptrcl  13389  lo1mptrcl  13403  o1mptrcl  13404  o1fsum  13586  ram0  14395  funcres  15119  curf2cl  15354  uncfcurf  15362  yonedalem4c  15400  resmhm  15800  gsumprval  15827  gsumwsubmcl  15829  gsumccat  15832  gsumwmhm  15836  frmdup1  15855  frmdup3  15857  isghm  16062  resghm  16078  subgga  16133  gasubg  16135  psgnunilem2  16316  sylow2blem2  16437  pj2f  16512  pj1ghm  16517  frgpupf  16587  frgpup3lem  16591  gsumval3OLD  16699  gsumval3  16702  gsummptfzcl  16787  dprdf2  16831  ablfaclem2  16927  ablfac2  16930  isabvd  17252  abvpropd  17274  mplasclf  17933  evlssca  17962  lply1binomsc  18120  cygznlem2a  18373  frgpcyg  18379  mat1dimelbas  18740  mat2pmatbas  18994  cpmadugsumlemF  19144  cnpf2  19517  lmcnp  19571  ptpjcn  19847  pt1hmeo  20042  cnextfres  20303  cnmpt2pc  21163  pi1addf  21282  pi1xfrf  21288  pi1cof  21294  mbfmptcl  21779  iblcnlem  21930  limcres  22025  cnplimc  22026  limccnp  22030  limccnp2  22031  limcun  22034  dvidlem  22054  cpnord  22073  dvaddf  22080  dvmulf  22081  dvcmulf  22083  dvcof  22086  dvcj  22088  dvrec  22093  dvmptcl  22097  dvcnvlem  22112  dvcnv  22113  rolle  22126  cmvth  22127  mvth  22128  dvlip  22129  dvlipcn  22130  c1lip2  22134  dv11cn  22137  dvivthlem1  22144  dvivthlem2  22145  dvivth  22146  dvne0  22147  lhop1lem  22149  lhop1  22150  lhop2  22151  lhop  22152  dvcnvrelem2  22154  taylthlem1  22502  taylthlem2  22503  ulmf2  22513  ulm2  22514  ulmdv  22532  pserdv  22558  rlimcxp  23031  o1cxp  23032  dchrptlem2  23268  axlowdimlem5  23925  axlowdimlem7  23927  axlowdimlem10  23930  uhgraun  23987  wrdumgra  23992  umgraf  23994  umgra1  24002  umgraun  24004  wlkelwrd  24206  2trllemH  24230  2trllemG  24236  is2wlk  24243  redwlk  24284  usgra2adedgwlkonALT  24292  usgra2wlkspthlem1  24295  usgra2wlkspthlem2  24296  fargshiftf  24312  3v3e3cycl1  24320  4cycl4v4e  24342  4cycl4dv  24343  4cycl4dv4e  24344  wlkiswwlk2lem3  24369  wlkiswwlk2  24373  vfwlkniswwlkn  24382  clwlkisclwwlklem2a  24461  clwlkisclwwlklem2  24462  clwlkfclwwlk2wrd  24516  clwlkf1clwwlklem3  24524  el2wlkonotlem  24538  eupai  24643  eupatrl  24644  eupa0  24650  eupares  24651  eupap1  24652  isgrpo  24874  elghomlem1  25039  rngosn3  25104  vci  25117  isvclem  25146  vcoprnelem  25147  isnvlem  25179  ajfval  25400  1stmbfm  27871  2ndmbfm  27872  sibfof  27922  rrvf2  28027  signshf  28185  cvmliftmolem1  28366  cvmliftlem7  28376  cvmliftlem10  28379  cvmlift2lem9  28396  filnetlem4  29802  sdclem2  29838  sdclem1  29839  sdc  29840  fdc  29841  sstotbnd2  29873  cncfuni  31225  cncfiooicclem1  31232  dvsubf  31242  dvdivf  31252  dvbdfbdioolem1  31258  ioodvbdlimc1lem1  31261  ioodvbdlimc1lem2  31262  ioodvbdlimc1  31263  ioodvbdlimc2lem  31264  ioodvbdlimc2  31265  itgsubsticclem  31293  fourierdlem45  31452  fourierdlem48  31455  fourierdlem49  31456  fourierdlem58  31465  fourierdlem59  31466  fourierdlem69  31476  fourierdlem75  31482  fourierdlem89  31496  fourierdlem91  31498  fourierdlem97  31504  fourierdlem113  31520  2ffzoeq  31810  usgra2pthspth  31820  usgra2pthlem1  31822  usgra2pth  31823  uhgun  31849
  Copyright terms: Public domain W3C validator