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

Theorem feq2d 5380
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 5376 . 2  |-  ( A  =  B  ->  ( F : A --> C  <->  F : B
--> C ) )
31, 2syl 15 1  |-  ( ph  ->  ( F : A --> C 
<->  F : B --> C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1623   -->wf 5251
This theorem is referenced by:  feq12d  5381  ffdm  5403  fsng  5697  fsnunf2  5719  issmo2  6366  qliftf  6746  elpm2r  6788  ordtypelem5  7237  axdc3lem3  8078  axdc3lem4  8079  fseq1p1m1  10857  fseq1m1p1  10858  seqf1o  11087  iswrdi  11417  wrdf  11419  eqs1  11447  cats1un  11476  rlimi  11987  rlimmptrcl  12081  lo1mptrcl  12095  o1mptrcl  12096  o1fsum  12271  ram0  13069  funcres  13770  curf2cl  14005  uncfcurf  14013  yonedalem4c  14051  resmhm  14436  gsumwsubmcl  14461  gsumccat  14464  gsumwmhm  14467  frmdup1  14486  frmdup3  14488  isghm  14683  resghm  14699  subgga  14754  gasubg  14756  sylow2blem2  14932  pj2f  15007  pj1ghm  15012  frgpupf  15082  frgpup3lem  15086  gsumval3  15191  dprdf2  15242  ablfaclem2  15321  ablfac2  15324  isabvd  15585  abvpropd  15607  mplasclf  16238  cygznlem2a  16521  frgpcyg  16527  cnpf2  16980  lmcnp  17032  ptpjcn  17305  pt1hmeo  17497  cnmpt2pc  18426  pi1addf  18545  pi1xfrf  18551  pi1cof  18557  mbfmptcl  18992  iblcnlem  19143  limcres  19236  cnplimc  19237  limccnp  19241  limccnp2  19242  limcun  19245  dvidlem  19265  cpnord  19284  dvaddf  19291  dvmulf  19292  dvcmulf  19294  dvcof  19297  dvcj  19299  dvrec  19304  dvmptcl  19308  dvcnvlem  19323  dvcnv  19324  rolle  19337  cmvth  19338  mvth  19339  dvlip  19340  dvlipcn  19341  c1lip2  19345  dv11cn  19348  dvivthlem1  19355  dvivthlem2  19356  dvivth  19357  dvne0  19358  lhop1lem  19360  lhop1  19361  lhop2  19362  lhop  19363  dvcnvrelem2  19365  evlssca  19406  taylthlem1  19752  taylthlem2  19753  ulmf2  19763  ulm2  19764  ulmdv  19780  pserdv  19805  rlimcxp  20268  o1cxp  20269  dchrptlem2  20504  isgrpo  20863  elghomlem1  21028  rngosn3  21093  vci  21104  isvclem  21133  vcoprnelem  21134  isnvlem  21166  ajfval  21387  1stmbfm  23565  2ndmbfm  23566  rrvf2  23651  cvmliftmolem1  23812  cvmliftlem7  23822  cvmliftlem10  23825  cvmlift2lem9  23842  wrdumgra  23868  umgraf  23870  umgra1  23878  umgraun  23879  eupai  23883  eupa0  23898  eupares  23899  eupap1  23900  axlowdimlem5  24574  axlowdimlem7  24576  axlowdimlem10  24579  cbicp  25166  vecval1b  25451  vecval3b  25452  intopcoaconb  25540  istopx  25547  prcnt  25551  ismgra  25710  isalg  25721  algi  25727  dualalg  25782  1iskle  25989  clscnc  26010  filnetlem4  26330  sdclem2  26452  sdclem1  26453  sdc  26454  fdc  26455  sstotbnd2  26498  ralxpmap  26761  psgnunilem2  27418  uslgraun  28120
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2276  df-fn 5258  df-f 5259
  Copyright terms: Public domain W3C validator