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

Theorem feq2d 5733
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 5729 . 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 187    = wceq 1437   -->wf 5597
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-cleq 2421  df-fn 5604  df-f 5605
This theorem is referenced by:  feq12d  5735  ffdm  5760  fsng  6078  fsn2g  6079  fsnunf2  6118  issmo2  7076  qliftf  7459  elpm2r  7497  ralxpmap  7529  ordtypelem5  8037  axdc3lem3  8880  axdc3lem4  8881  fseq1p1m1  11866  fseq1m1p1  11867  seqf1o  12251  iswrdi  12662  wrdf  12663  snopiswrd  12668  ffz0iswrd  12681  wrdnval  12684  swrdf  12766  swrd0f  12768  cats1un  12817  cshwf  12887  wrdlen2i  13000  wrd2pr2op  13001  wwlktovf  13010  rlimi  13555  rlimmptrcl  13649  lo1mptrcl  13663  o1mptrcl  13664  o1fsum  13851  ram0  14943  funcres  15752  curf2cl  16067  uncfcurf  16075  yonedalem4c  16113  intopsn  16449  gsumprval  16475  resmhm  16557  gsumwsubmcl  16573  gsumccat  16576  gsumwmhm  16580  frmdup1  16599  frmdup3lem  16601  isghm  16834  resghm  16850  subgga  16905  gasubg  16907  psgnunilem2  17087  sylow2blem2  17208  pj2f  17283  pj1ghm  17288  frgpupf  17358  frgpup3lem  17362  gsumval3  17476  gsummptfzcl  17536  dprdf2  17574  ablfaclem2  17654  ablfac2  17657  isabvd  17983  abvpropd  18005  mplasclf  18655  evlssca  18680  lply1binomsc  18836  cygznlem2a  19069  frgpcyg  19075  mat1dimelbas  19427  mat2pmatbas  19681  cpmadugsumlemF  19831  cnpf2  20197  lmcnp  20251  ptpjcn  20557  pt1hmeo  20752  cnextfres1  21014  cnextfres  21015  cnmpt2pc  21852  pi1addf  21971  pi1xfrf  21977  pi1cof  21983  mbfmptcl  22470  iblcnlem  22623  limcres  22718  cnplimc  22719  limccnp  22723  limccnp2  22724  limcun  22727  dvidlem  22747  cpnord  22766  dvaddf  22773  dvmulf  22774  dvcmulf  22776  dvcof  22779  dvcj  22781  dvrec  22786  dvmptcl  22790  dvcnvlem  22805  dvcnv  22806  rolle  22819  cmvth  22820  mvth  22821  dvlip  22822  dvlipcn  22823  c1lip2  22827  dv11cn  22830  dvivthlem1  22837  dvivthlem2  22838  dvivth  22839  dvne0  22840  lhop1lem  22842  lhop1  22843  lhop2  22844  lhop  22845  dvcnvrelem2  22847  taylthlem1  23193  taylthlem2  23194  ulmf2  23204  ulm2  23205  ulmdv  23223  pserdv  23249  rlimcxp  23764  o1cxp  23765  dchrptlem2  24056  axlowdimlem5  24822  axlowdimlem7  24824  axlowdimlem10  24827  uhgraun  24884  wrdumgra  24889  umgraf  24891  umgra1  24899  umgraun  24901  wlkelwrd  25103  2trllemH  25127  2trllemG  25133  is2wlk  25140  redwlk  25181  usgra2adedgwlkonALT  25189  usgra2wlkspthlem1  25192  usgra2wlkspthlem2  25193  fargshiftf  25209  3v3e3cycl1  25217  4cycl4v4e  25239  4cycl4dv  25240  4cycl4dv4e  25241  wlkiswwlk2lem3  25266  wlkiswwlk2  25270  vfwlkniswwlkn  25279  clwlkisclwwlklem2a  25358  clwlkisclwwlklem2  25359  clwlkfclwwlk2wrd  25413  clwlkf1clwwlklem3  25421  el2wlkonotlem  25435  eupai  25540  eupatrl  25541  eupa0  25547  eupares  25548  eupap1  25549  isgrpo  25769  elghomlem1OLD  25934  rngosn3  25999  vci  26012  isvclem  26041  vcoprnelem  26042  isnvlem  26074  ajfval  26295  acunirnmpt2  28102  acunirnmpt2f  28103  smatrcl  28461  locfinref  28507  1stmbfm  28921  2ndmbfm  28922  sibfof  29001  rrvf2  29107  signshf  29265  cvmliftmolem1  29792  cvmliftlem7  29802  cvmliftlem10  29805  cvmlift2lem9  29822  filnetlem4  30822  poimirlem16  31660  poimirlem19  31663  poimirlem23  31667  poimirlem24  31668  poimirlem25  31669  poimirlem29  31673  poimirlem31  31675  sdclem2  31775  sdclem1  31776  sdc  31777  fdc  31778  sstotbnd2  31810  amgm4d  36289  mptelpm  37063  cncfuni  37336  cncfiooicclem1  37343  dvsubf  37356  dvdivf  37366  dvbdfbdioolem1  37372  ioodvbdlimc1lem1  37375  ioodvbdlimc1lem2  37376  ioodvbdlimc1  37377  ioodvbdlimc2lem  37378  ioodvbdlimc2  37379  dvnprodlem3  37392  itgsubsticclem  37421  fourierdlem48  37586  fourierdlem49  37587  fourierdlem58  37596  fourierdlem59  37597  fourierdlem60  37598  fourierdlem61  37599  fourierdlem69  37607  fourierdlem75  37613  fourierdlem81  37619  fourierdlem89  37627  fourierdlem91  37629  fourierdlem97  37635  fourierdlem113  37651  meaf  37800  ismeannd  37814  psmeasure  37818  omef  37826  2ffzoeq  38422  usgra2pthspth  38430  usgra2pthlem1  38432  usgra2pth  38433  uhgun  38459  resmgmhm  38565  elbigolo1  39138
  Copyright terms: Public domain W3C validator