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

Theorem feq2d 5540
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 5536 . 2  |-  ( A  =  B  ->  ( F : A --> C  <->  F : B
--> C ) )
31, 2syl 16 1  |-  ( ph  ->  ( F : A --> C 
<->  F : B --> C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649   -->wf 5409
This theorem is referenced by:  feq12d  5541  ffdm  5564  fsng  5866  fsnunf2  5891  issmo2  6570  qliftf  6951  elpm2r  6993  ordtypelem5  7447  axdc3lem3  8288  axdc3lem4  8289  fseq1p1m1  11077  fseq1m1p1  11078  seqf1o  11319  iswrdi  11686  wrdf  11688  eqs1  11716  cats1un  11745  rlimi  12262  rlimmptrcl  12356  lo1mptrcl  12370  o1mptrcl  12371  o1fsum  12547  ram0  13345  funcres  14048  curf2cl  14283  uncfcurf  14291  yonedalem4c  14329  resmhm  14714  gsumwsubmcl  14739  gsumccat  14742  gsumwmhm  14745  frmdup1  14764  frmdup3  14766  isghm  14961  resghm  14977  subgga  15032  gasubg  15034  sylow2blem2  15210  pj2f  15285  pj1ghm  15290  frgpupf  15360  frgpup3lem  15364  gsumval3  15469  dprdf2  15520  ablfaclem2  15599  ablfac2  15602  isabvd  15863  abvpropd  15885  mplasclf  16512  cygznlem2a  16803  frgpcyg  16809  cnpf2  17268  lmcnp  17322  ptpjcn  17596  pt1hmeo  17791  cnextfres  18052  cnmpt2pc  18906  pi1addf  19025  pi1xfrf  19031  pi1cof  19037  mbfmptcl  19482  iblcnlem  19633  limcres  19726  cnplimc  19727  limccnp  19731  limccnp2  19732  limcun  19735  dvidlem  19755  cpnord  19774  dvaddf  19781  dvmulf  19782  dvcmulf  19784  dvcof  19787  dvcj  19789  dvrec  19794  dvmptcl  19798  dvcnvlem  19813  dvcnv  19814  rolle  19827  cmvth  19828  mvth  19829  dvlip  19830  dvlipcn  19831  c1lip2  19835  dv11cn  19838  dvivthlem1  19845  dvivthlem2  19846  dvivth  19847  dvne0  19848  lhop1lem  19850  lhop1  19851  lhop2  19852  lhop  19853  dvcnvrelem2  19855  evlssca  19896  taylthlem1  20242  taylthlem2  20243  ulmf2  20253  ulm2  20254  ulmdv  20272  pserdv  20298  rlimcxp  20765  o1cxp  20766  dchrptlem2  21002  uhgraun  21299  wrdumgra  21304  umgraf  21306  umgra1  21314  umgraun  21316  2trllemH  21505  2trllemG  21511  is2wlk  21518  redwlk  21559  fargshiftf  21576  3v3e3cycl1  21584  4cycl4v4e  21606  4cycl4dv  21607  4cycl4dv4e  21608  eupai  21642  eupatrl  21643  eupa0  21649  eupares  21650  eupap1  21651  isgrpo  21737  elghomlem1  21902  rngosn3  21967  vci  21980  isvclem  22009  vcoprnelem  22010  isnvlem  22042  ajfval  22263  1stmbfm  24563  2ndmbfm  24564  sibfof  24607  rrvf2  24659  cvmliftmolem1  24921  cvmliftlem7  24931  cvmliftlem10  24934  cvmlift2lem9  24951  axlowdimlem5  25789  axlowdimlem7  25791  axlowdimlem10  25794  filnetlem4  26300  sdclem2  26336  sdclem1  26337  sdc  26338  fdc  26339  sstotbnd2  26373  ralxpmap  26632  psgnunilem2  27286  iswrd0i  27999  usgra2pthspth  28035  usgra2wlkspthlem1  28036  usgra2wlkspthlem2  28037  usgra2pthlem1  28040  usgra2pth  28041  el2wlkonotlem  28059
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  df-fn 5416  df-f 5417
  Copyright terms: Public domain W3C validator