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

Theorem feq2d 5739
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 5735 . 2  |-  ( A  =  B  ->  ( F : A --> C  <->  F : B
--> C ) )
31, 2syl 17 1  |-  ( ph  ->  ( F : A --> C 
<->  F : B --> C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    = wceq 1438   -->wf 5603
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1664  ax-4 1677  ax-ext 2402
This theorem depends on definitions:  df-bi 189  df-an 373  df-cleq 2415  df-fn 5610  df-f 5611
This theorem is referenced by:  feq12d  5741  ffdm  5766  fsng  6084  fsn2g  6085  fsnunf2  6124  issmo2  7085  qliftf  7468  elpm2r  7506  ralxpmap  7538  ordtypelem5  8052  axdc3lem3  8895  axdc3lem4  8896  fseq1p1m1  11881  fseq1m1p1  11882  seqf1o  12266  iswrdi  12685  wrdf  12686  snopiswrd  12691  ffz0iswrd  12704  wrdnval  12707  swrdf  12789  swrd0f  12791  cats1un  12840  cshwf  12910  wrdlen2i  13027  wrd2pr2op  13028  wwlktovf  13037  rlimi  13582  rlimmptrcl  13676  lo1mptrcl  13690  o1mptrcl  13691  o1fsum  13878  ram0  14985  funcres  15806  curf2cl  16121  uncfcurf  16129  yonedalem4c  16167  intopsn  16503  gsumprval  16529  resmhm  16611  gsumwsubmcl  16627  gsumccat  16630  gsumwmhm  16634  frmdup1  16653  frmdup3lem  16655  isghm  16888  resghm  16904  subgga  16959  gasubg  16961  psgnunilem2  17141  sylow2blem2  17278  pj2f  17353  pj1ghm  17358  frgpupf  17428  frgpup3lem  17432  gsumval3  17546  gsummptfzcl  17606  dprdf2  17644  ablfaclem2  17724  ablfac2  17727  isabvd  18053  abvpropd  18075  mplasclf  18725  evlssca  18750  lply1binomsc  18906  cygznlem2a  19142  frgpcyg  19148  mat1dimelbas  19500  mat2pmatbas  19754  cpmadugsumlemF  19904  cnpf2  20270  lmcnp  20324  ptpjcn  20630  pt1hmeo  20825  cnextfres1  21087  cnextfres  21088  cnmpt2pc  21960  pi1addf  22082  pi1xfrf  22088  pi1cof  22094  mbfmptcl  22597  iblcnlem  22750  limcres  22845  cnplimc  22846  limccnp  22850  limccnp2  22851  limcun  22854  dvidlem  22874  cpnord  22893  dvaddf  22900  dvmulf  22901  dvcmulf  22903  dvcof  22906  dvcj  22908  dvrec  22913  dvmptcl  22917  dvcnvlem  22932  dvcnv  22933  rolle  22946  cmvth  22947  mvth  22948  dvlip  22949  dvlipcn  22950  c1lip2  22954  dv11cn  22957  dvivthlem1  22964  dvivthlem2  22965  dvivth  22966  dvne0  22967  lhop1lem  22969  lhop1  22970  lhop2  22971  lhop  22972  dvcnvrelem2  22974  taylthlem1  23332  taylthlem2  23333  ulmf2  23343  ulm2  23344  ulmdv  23362  pserdv  23388  rlimcxp  23903  o1cxp  23904  dchrptlem2  24197  axlowdimlem5  24980  axlowdimlem7  24982  axlowdimlem10  24985  uhgraun  25042  wrdumgra  25047  umgraf  25049  umgra1  25057  umgraun  25059  wlkelwrd  25262  2trllemH  25286  2trllemG  25292  is2wlk  25299  redwlk  25340  usgra2adedgwlkonALT  25348  usgra2wlkspthlem1  25351  usgra2wlkspthlem2  25352  fargshiftf  25368  3v3e3cycl1  25376  4cycl4v4e  25398  4cycl4dv  25399  4cycl4dv4e  25400  wlkiswwlk2lem3  25425  wlkiswwlk2  25429  vfwlkniswwlkn  25438  clwlkisclwwlklem2a  25517  clwlkisclwwlklem2  25518  clwlkfclwwlk2wrd  25572  clwlkf1clwwlklem3  25580  el2wlkonotlem  25594  eupai  25699  eupatrl  25700  eupa0  25706  eupares  25707  eupap1  25708  isgrpo  25928  elghomlem1OLD  26093  rngosn3  26158  vci  26171  isvclem  26200  vcoprnelem  26201  isnvlem  26233  ajfval  26454  acunirnmpt2  28270  acunirnmpt2f  28271  smatrcl  28636  locfinref  28682  1stmbfm  29096  2ndmbfm  29097  sibfof  29187  rrvf2  29295  signshf  29491  cvmliftmolem1  30018  cvmliftlem7  30028  cvmliftlem10  30031  cvmlift2lem9  30048  filnetlem4  31048  poimirlem16  31926  poimirlem19  31929  poimirlem23  31933  poimirlem24  31934  poimirlem25  31935  poimirlem29  31939  poimirlem31  31941  sdclem2  32041  sdclem1  32042  sdc  32043  fdc  32044  sstotbnd2  32076  amgm4d  36628  mptelpm  37407  cncfuni  37710  cncfiooicclem1  37717  dvsubf  37730  dvdivf  37740  dvbdfbdioolem1  37746  ioodvbdlimc1lem1  37749  ioodvbdlimc1lem2  37750  ioodvbdlimc1lem1OLD  37751  ioodvbdlimc1lem2OLD  37752  ioodvbdlimc1  37753  ioodvbdlimc2lem  37754  ioodvbdlimc2lemOLD  37755  ioodvbdlimc2  37756  dvnprodlem3  37769  itgsubsticclem  37798  fourierdlem48  37964  fourierdlem49  37965  fourierdlem58  37974  fourierdlem59  37975  fourierdlem60  37976  fourierdlem61  37977  fourierdlem69  37985  fourierdlem75  37991  fourierdlem81  37997  fourierdlem89  38005  fourierdlem91  38007  fourierdlem97  38013  fourierdlem113  38029  meaf  38205  ismeannd  38219  psmeasure  38223  omef  38231  isomennd  38266  hoidmvlelem2  38328  hoidmvlelem3  38329  ovnhoi  38335  2ffzoeq  38923  uhgrn0  38990  uhgrunlem  39001  uhgrun  39002  wrdumgr  39009  umgrf  39011  umgr1  39019  umgrun  39025  umgrres1  39146  usgra2pthspth  39282  usgra2pthlem1  39284  usgra2pth  39285  uhgun  39309  resmgmhm  39415  elbigolo1  39987
  Copyright terms: Public domain W3C validator