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

Theorem feq2d 5396
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 5392 . 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 1632   -->wf 5267
This theorem is referenced by:  feq12d  5397  ffdm  5419  fsng  5713  fsnunf2  5735  issmo2  6382  qliftf  6762  elpm2r  6804  ordtypelem5  7253  axdc3lem3  8094  axdc3lem4  8095  fseq1p1m1  10873  fseq1m1p1  10874  seqf1o  11103  iswrdi  11433  wrdf  11435  eqs1  11463  cats1un  11492  rlimi  12003  rlimmptrcl  12097  lo1mptrcl  12111  o1mptrcl  12112  o1fsum  12287  ram0  13085  funcres  13786  curf2cl  14021  uncfcurf  14029  yonedalem4c  14067  resmhm  14452  gsumwsubmcl  14477  gsumccat  14480  gsumwmhm  14483  frmdup1  14502  frmdup3  14504  isghm  14699  resghm  14715  subgga  14770  gasubg  14772  sylow2blem2  14948  pj2f  15023  pj1ghm  15028  frgpupf  15098  frgpup3lem  15102  gsumval3  15207  dprdf2  15258  ablfaclem2  15337  ablfac2  15340  isabvd  15601  abvpropd  15623  mplasclf  16254  cygznlem2a  16537  frgpcyg  16543  cnpf2  16996  lmcnp  17048  ptpjcn  17321  pt1hmeo  17513  cnmpt2pc  18442  pi1addf  18561  pi1xfrf  18567  pi1cof  18573  mbfmptcl  19008  iblcnlem  19159  limcres  19252  cnplimc  19253  limccnp  19257  limccnp2  19258  limcun  19261  dvidlem  19281  cpnord  19300  dvaddf  19307  dvmulf  19308  dvcmulf  19310  dvcof  19313  dvcj  19315  dvrec  19320  dvmptcl  19324  dvcnvlem  19339  dvcnv  19340  rolle  19353  cmvth  19354  mvth  19355  dvlip  19356  dvlipcn  19357  c1lip2  19361  dv11cn  19364  dvivthlem1  19371  dvivthlem2  19372  dvivth  19373  dvne0  19374  lhop1lem  19376  lhop1  19377  lhop2  19378  lhop  19379  dvcnvrelem2  19381  evlssca  19422  taylthlem1  19768  taylthlem2  19769  ulmf2  19779  ulm2  19780  ulmdv  19796  pserdv  19821  rlimcxp  20284  o1cxp  20285  dchrptlem2  20520  isgrpo  20879  elghomlem1  21044  rngosn3  21109  vci  21120  isvclem  21149  vcoprnelem  21150  isnvlem  21182  ajfval  21403  1stmbfm  23580  2ndmbfm  23581  rrvf2  23666  cvmliftmolem1  23827  cvmliftlem7  23837  cvmliftlem10  23840  cvmlift2lem9  23857  wrdumgra  23883  umgraf  23885  umgra1  23893  umgraun  23894  eupai  23898  eupa0  23913  eupares  23914  eupap1  23915  axlowdimlem5  24646  axlowdimlem7  24648  axlowdimlem10  24651  cbicp  25269  vecval1b  25554  vecval3b  25555  intopcoaconb  25643  istopx  25650  prcnt  25654  ismgra  25813  isalg  25824  algi  25830  dualalg  25885  1iskle  26092  clscnc  26113  filnetlem4  26433  sdclem2  26555  sdclem1  26556  sdc  26557  fdc  26558  sstotbnd2  26601  ralxpmap  26864  psgnunilem2  27521  uslgraun  28254  redwlk  28364  fargshiftf  28381  eupatrl  28385  3v3e3cycl1  28390  4cycl4v4e  28412  4cycl4dv  28413  4cycl4dv4e  28414
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2289  df-fn 5274  df-f 5275
  Copyright terms: Public domain W3C validator