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

Theorem feq2d 5581
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 5577 . 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 1652   -->wf 5450
This theorem is referenced by:  feq12d  5582  ffdm  5605  fsng  5907  fsnunf2  5932  issmo2  6611  qliftf  6992  elpm2r  7034  ordtypelem5  7491  axdc3lem3  8332  axdc3lem4  8333  fseq1p1m1  11122  fseq1m1p1  11123  seqf1o  11364  iswrdi  11731  wrdf  11733  eqs1  11761  cats1un  11790  rlimi  12307  rlimmptrcl  12401  lo1mptrcl  12415  o1mptrcl  12416  o1fsum  12592  ram0  13390  funcres  14093  curf2cl  14328  uncfcurf  14336  yonedalem4c  14374  resmhm  14759  gsumwsubmcl  14784  gsumccat  14787  gsumwmhm  14790  frmdup1  14809  frmdup3  14811  isghm  15006  resghm  15022  subgga  15077  gasubg  15079  sylow2blem2  15255  pj2f  15330  pj1ghm  15335  frgpupf  15405  frgpup3lem  15409  gsumval3  15514  dprdf2  15565  ablfaclem2  15644  ablfac2  15647  isabvd  15908  abvpropd  15930  mplasclf  16557  cygznlem2a  16848  frgpcyg  16854  cnpf2  17314  lmcnp  17368  ptpjcn  17643  pt1hmeo  17838  cnextfres  18099  cnmpt2pc  18953  pi1addf  19072  pi1xfrf  19078  pi1cof  19084  mbfmptcl  19529  iblcnlem  19680  limcres  19773  cnplimc  19774  limccnp  19778  limccnp2  19779  limcun  19782  dvidlem  19802  cpnord  19821  dvaddf  19828  dvmulf  19829  dvcmulf  19831  dvcof  19834  dvcj  19836  dvrec  19841  dvmptcl  19845  dvcnvlem  19860  dvcnv  19861  rolle  19874  cmvth  19875  mvth  19876  dvlip  19877  dvlipcn  19878  c1lip2  19882  dv11cn  19885  dvivthlem1  19892  dvivthlem2  19893  dvivth  19894  dvne0  19895  lhop1lem  19897  lhop1  19898  lhop2  19899  lhop  19900  dvcnvrelem2  19902  evlssca  19943  taylthlem1  20289  taylthlem2  20290  ulmf2  20300  ulm2  20301  ulmdv  20319  pserdv  20345  rlimcxp  20812  o1cxp  20813  dchrptlem2  21049  uhgraun  21346  wrdumgra  21351  umgraf  21353  umgra1  21361  umgraun  21363  2trllemH  21552  2trllemG  21558  is2wlk  21565  redwlk  21606  fargshiftf  21623  3v3e3cycl1  21631  4cycl4v4e  21653  4cycl4dv  21654  4cycl4dv4e  21655  eupai  21689  eupatrl  21690  eupa0  21696  eupares  21697  eupap1  21698  isgrpo  21784  elghomlem1  21949  rngosn3  22014  vci  22027  isvclem  22056  vcoprnelem  22057  isnvlem  22089  ajfval  22310  1stmbfm  24610  2ndmbfm  24611  sibfof  24654  rrvf2  24706  cvmliftmolem1  24968  cvmliftlem7  24978  cvmliftlem10  24981  cvmlift2lem9  24998  axlowdimlem5  25885  axlowdimlem7  25887  axlowdimlem10  25890  filnetlem4  26410  sdclem2  26446  sdclem1  26447  sdc  26448  fdc  26449  sstotbnd2  26483  ralxpmap  26742  psgnunilem2  27395  2ffzoeq  28140  iswrd0i  28169  wlkelwrd  28295  usgra2pthspth  28305  usgra2wlkspthlem1  28306  usgra2wlkspthlem2  28307  usgra2pthlem1  28310  usgra2pth  28311  el2wlkonotlem  28329
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2429  df-fn 5457  df-f 5458
  Copyright terms: Public domain W3C validator