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

Theorem feq2d 5704
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 5700 . 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 1381   -->wf 5570
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2433  df-fn 5577  df-f 5578
This theorem is referenced by:  feq12d  5706  ffdm  5731  fsng  6051  fsnunf2  6091  issmo2  7018  qliftf  7397  elpm2r  7434  ralxpmap  7466  ordtypelem5  7945  axdc3lem3  8830  axdc3lem4  8831  fseq1p1m1  11756  fseq1m1p1  11757  seqf1o  12122  iswrdi  12526  wrdf  12527  snopiswrd  12530  ffz0iswrd  12542  wrdnval  12545  eqs1  12595  swrdf  12627  cats1un  12675  cshwf  12745  wrdlen2i  12858  wrd2pr2op  12859  wwlktovf  12868  rlimi  13310  rlimmptrcl  13404  lo1mptrcl  13418  o1mptrcl  13419  o1fsum  13601  ram0  14412  funcres  15134  curf2cl  15369  uncfcurf  15377  yonedalem4c  15415  intopsn  15751  gsumprval  15777  resmhm  15859  gsumwsubmcl  15875  gsumccat  15878  gsumwmhm  15882  frmdup1  15901  frmdup3lem  15903  isghm  16136  resghm  16152  subgga  16207  gasubg  16209  psgnunilem2  16389  sylow2blem2  16510  pj2f  16585  pj1ghm  16590  frgpupf  16660  frgpup3lem  16664  gsumval3OLD  16777  gsumval3  16780  gsummptfzcl  16865  dprdf2  16909  ablfaclem2  17005  ablfac2  17008  isabvd  17337  abvpropd  17359  mplasclf  18030  evlssca  18059  lply1binomsc  18217  cygznlem2a  18473  frgpcyg  18479  mat1dimelbas  18840  mat2pmatbas  19094  cpmadugsumlemF  19244  cnpf2  19617  lmcnp  19671  ptpjcn  19978  pt1hmeo  20173  cnextfres  20434  cnmpt2pc  21294  pi1addf  21413  pi1xfrf  21419  pi1cof  21425  mbfmptcl  21910  iblcnlem  22061  limcres  22156  cnplimc  22157  limccnp  22161  limccnp2  22162  limcun  22165  dvidlem  22185  cpnord  22204  dvaddf  22211  dvmulf  22212  dvcmulf  22214  dvcof  22217  dvcj  22219  dvrec  22224  dvmptcl  22228  dvcnvlem  22243  dvcnv  22244  rolle  22257  cmvth  22258  mvth  22259  dvlip  22260  dvlipcn  22261  c1lip2  22265  dv11cn  22268  dvivthlem1  22275  dvivthlem2  22276  dvivth  22277  dvne0  22278  lhop1lem  22280  lhop1  22281  lhop2  22282  lhop  22283  dvcnvrelem2  22285  taylthlem1  22633  taylthlem2  22634  ulmf2  22644  ulm2  22645  ulmdv  22663  pserdv  22689  rlimcxp  23168  o1cxp  23169  dchrptlem2  23405  axlowdimlem5  24114  axlowdimlem7  24116  axlowdimlem10  24119  uhgraun  24176  wrdumgra  24181  umgraf  24183  umgra1  24191  umgraun  24193  wlkelwrd  24395  2trllemH  24419  2trllemG  24425  is2wlk  24432  redwlk  24473  usgra2adedgwlkonALT  24481  usgra2wlkspthlem1  24484  usgra2wlkspthlem2  24485  fargshiftf  24501  3v3e3cycl1  24509  4cycl4v4e  24531  4cycl4dv  24532  4cycl4dv4e  24533  wlkiswwlk2lem3  24558  wlkiswwlk2  24562  vfwlkniswwlkn  24571  clwlkisclwwlklem2a  24650  clwlkisclwwlklem2  24651  clwlkfclwwlk2wrd  24705  clwlkf1clwwlklem3  24713  el2wlkonotlem  24727  eupai  24832  eupatrl  24833  eupa0  24839  eupares  24840  eupap1  24841  isgrpo  25063  elghomlem1OLD  25228  rngosn3  25293  vci  25306  isvclem  25335  vcoprnelem  25336  isnvlem  25368  ajfval  25589  locfinref  27710  1stmbfm  28097  2ndmbfm  28098  sibfof  28148  rrvf2  28253  signshf  28411  cvmliftmolem1  28592  cvmliftlem7  28602  cvmliftlem10  28605  cvmlift2lem9  28622  filnetlem4  30167  sdclem2  30203  sdclem1  30204  sdc  30205  fdc  30206  sstotbnd2  30238  cncfuni  31592  cncfiooicclem1  31599  dvsubf  31609  dvdivf  31619  dvbdfbdioolem1  31625  ioodvbdlimc1lem1  31628  ioodvbdlimc1lem2  31629  ioodvbdlimc1  31630  ioodvbdlimc2lem  31631  ioodvbdlimc2  31632  itgsubsticclem  31660  fourierdlem48  31822  fourierdlem49  31823  fourierdlem58  31832  fourierdlem59  31833  fourierdlem60  31834  fourierdlem61  31835  fourierdlem69  31843  fourierdlem75  31849  fourierdlem81  31855  fourierdlem89  31863  fourierdlem91  31865  fourierdlem97  31871  fourierdlem113  31887  2ffzoeq  32175  usgra2pthspth  32185  usgra2pthlem1  32187  usgra2pth  32188  uhgun  32214  resmgmhm  32320
  Copyright terms: Public domain W3C validator