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

Theorem feq2d 5552
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 5548 . 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 1369   -->wf 5419
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2436  df-fn 5426  df-f 5427
This theorem is referenced by:  feq12d  5553  ffdm  5577  fsng  5887  fsnunf2  5922  issmo2  6815  qliftf  7193  elpm2r  7235  ralxpmap  7267  ordtypelem5  7741  axdc3lem3  8626  axdc3lem4  8627  fseq1p1m1  11539  fseq1m1p1  11540  seqf1o  11852  iswrdi  12244  wrdf  12245  snopiswrd  12248  ffz0iswrd  12260  wrdlenfi  12263  eqs1  12305  swrdf  12327  cats1un  12375  cshwf  12442  wrdlen2i  12551  wrd2pr2op  12552  rlimi  12996  rlimmptrcl  13090  lo1mptrcl  13104  o1mptrcl  13105  o1fsum  13281  ram0  14088  funcres  14811  curf2cl  15046  uncfcurf  15054  yonedalem4c  15092  resmhm  15492  gsumprval  15519  gsumwsubmcl  15521  gsumccat  15524  gsumwmhm  15528  frmdup1  15547  frmdup3  15549  isghm  15752  resghm  15768  subgga  15823  gasubg  15825  psgnunilem2  16006  sylow2blem2  16125  pj2f  16200  pj1ghm  16205  frgpupf  16275  frgpup3lem  16279  gsumval3OLD  16387  gsumval3  16390  gsummptfzcl  16465  dprdf2  16496  ablfaclem2  16592  ablfac2  16595  isabvd  16910  abvpropd  16932  mplasclf  17584  evlssca  17613  cygznlem2a  18005  frgpcyg  18011  cnpf2  18859  lmcnp  18913  ptpjcn  19189  pt1hmeo  19384  cnextfres  19645  cnmpt2pc  20505  pi1addf  20624  pi1xfrf  20630  pi1cof  20636  mbfmptcl  21120  iblcnlem  21271  limcres  21366  cnplimc  21367  limccnp  21371  limccnp2  21372  limcun  21375  dvidlem  21395  cpnord  21414  dvaddf  21421  dvmulf  21422  dvcmulf  21424  dvcof  21427  dvcj  21429  dvrec  21434  dvmptcl  21438  dvcnvlem  21453  dvcnv  21454  rolle  21467  cmvth  21468  mvth  21469  dvlip  21470  dvlipcn  21471  c1lip2  21475  dv11cn  21478  dvivthlem1  21485  dvivthlem2  21486  dvivth  21487  dvne0  21488  lhop1lem  21490  lhop1  21491  lhop2  21492  lhop  21493  dvcnvrelem2  21495  taylthlem1  21843  taylthlem2  21844  ulmf2  21854  ulm2  21855  ulmdv  21873  pserdv  21899  rlimcxp  22372  o1cxp  22373  dchrptlem2  22609  axlowdimlem5  23197  axlowdimlem7  23199  axlowdimlem10  23202  uhgraun  23250  wrdumgra  23255  umgraf  23257  umgra1  23265  umgraun  23267  2trllemH  23456  2trllemG  23462  is2wlk  23469  redwlk  23510  fargshiftf  23527  3v3e3cycl1  23535  4cycl4v4e  23557  4cycl4dv  23558  4cycl4dv4e  23559  eupai  23593  eupatrl  23594  eupa0  23600  eupares  23601  eupap1  23602  isgrpo  23688  elghomlem1  23853  rngosn3  23918  vci  23931  isvclem  23960  vcoprnelem  23961  isnvlem  23993  ajfval  24214  1stmbfm  26680  2ndmbfm  26681  sibfof  26731  rrvf2  26836  signshf  26994  cvmliftmolem1  27175  cvmliftlem7  27185  cvmliftlem10  27188  cvmlift2lem9  27205  filnetlem4  28607  sdclem2  28643  sdclem1  28644  sdc  28645  fdc  28646  sstotbnd2  28678  2ffzoeq  30219  wwlktovf  30256  wlkelwrd  30285  usgra2pthspth  30300  usgra2wlkspthlem1  30301  usgra2wlkspthlem2  30302  usgra2pthlem1  30305  usgra2pth  30306  wlkiswwlk2lem3  30332  wlkiswwlk2  30336  vfwlkniswwlkn  30345  el2wlkonotlem  30386  clwlkisclwwlklem2a  30452  clwlkisclwwlklem2  30453  wrdnval  30479  clwlkfclwwlk2wrd  30518  clwlkf1clwwlklem3  30526  lply1binomsc  30857  mat1dimelbas  30872
  Copyright terms: Public domain W3C validator