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

Theorem feq2d 5544
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 5540 . 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 1364   -->wf 5411
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-12 1797  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-cleq 2434  df-fn 5418  df-f 5419
This theorem is referenced by:  feq12d  5545  ffdm  5569  fsng  5879  fsnunf2  5914  issmo2  6806  qliftf  7184  elpm2r  7226  ralxpmap  7258  ordtypelem5  7732  axdc3lem3  8617  axdc3lem4  8618  fseq1p1m1  11530  fseq1m1p1  11531  seqf1o  11843  iswrdi  12235  wrdf  12236  snopiswrd  12239  ffz0iswrd  12251  wrdlenfi  12254  eqs1  12296  swrdf  12318  cats1un  12366  cshwf  12433  wrdlen2i  12542  wrd2pr2op  12543  rlimi  12987  rlimmptrcl  13081  lo1mptrcl  13095  o1mptrcl  13096  o1fsum  13272  ram0  14079  funcres  14802  curf2cl  15037  uncfcurf  15045  yonedalem4c  15083  resmhm  15482  gsumprval  15507  gsumwsubmcl  15509  gsumccat  15512  gsumwmhm  15516  frmdup1  15535  frmdup3  15537  isghm  15740  resghm  15756  subgga  15811  gasubg  15813  psgnunilem2  15994  sylow2blem2  16113  pj2f  16188  pj1ghm  16193  frgpupf  16263  frgpup3lem  16267  gsumval3OLD  16375  gsumval3  16378  gsummptfzcl  16450  dprdf2  16481  ablfaclem2  16577  ablfac2  16580  isabvd  16885  abvpropd  16907  mplasclf  17555  evlssca  17584  cygznlem2a  17959  frgpcyg  17965  cnpf2  18813  lmcnp  18867  ptpjcn  19143  pt1hmeo  19338  cnextfres  19599  cnmpt2pc  20459  pi1addf  20578  pi1xfrf  20584  pi1cof  20590  mbfmptcl  21074  iblcnlem  21225  limcres  21320  cnplimc  21321  limccnp  21325  limccnp2  21326  limcun  21329  dvidlem  21349  cpnord  21368  dvaddf  21375  dvmulf  21376  dvcmulf  21378  dvcof  21381  dvcj  21383  dvrec  21388  dvmptcl  21392  dvcnvlem  21407  dvcnv  21408  rolle  21421  cmvth  21422  mvth  21423  dvlip  21424  dvlipcn  21425  c1lip2  21429  dv11cn  21432  dvivthlem1  21439  dvivthlem2  21440  dvivth  21441  dvne0  21442  lhop1lem  21444  lhop1  21445  lhop2  21446  lhop  21447  dvcnvrelem2  21449  taylthlem1  21797  taylthlem2  21798  ulmf2  21808  ulm2  21809  ulmdv  21827  pserdv  21853  rlimcxp  22326  o1cxp  22327  dchrptlem2  22563  axlowdimlem5  23127  axlowdimlem7  23129  axlowdimlem10  23132  uhgraun  23180  wrdumgra  23185  umgraf  23187  umgra1  23195  umgraun  23197  2trllemH  23386  2trllemG  23392  is2wlk  23399  redwlk  23440  fargshiftf  23457  3v3e3cycl1  23465  4cycl4v4e  23487  4cycl4dv  23488  4cycl4dv4e  23489  eupai  23523  eupatrl  23524  eupa0  23530  eupares  23531  eupap1  23532  isgrpo  23618  elghomlem1  23783  rngosn3  23848  vci  23861  isvclem  23890  vcoprnelem  23891  isnvlem  23923  ajfval  24144  1stmbfm  26611  2ndmbfm  26612  sibfof  26656  rrvf2  26761  signshf  26919  cvmliftmolem1  27100  cvmliftlem7  27110  cvmliftlem10  27113  cvmlift2lem9  27130  filnetlem4  28527  sdclem2  28563  sdclem1  28564  sdc  28565  fdc  28566  sstotbnd2  28598  2ffzoeq  30139  wwlktovf  30176  wlkelwrd  30205  usgra2pthspth  30220  usgra2wlkspthlem1  30221  usgra2wlkspthlem2  30222  usgra2pthlem1  30225  usgra2pth  30226  wlkiswwlk2lem3  30252  wlkiswwlk2  30256  vfwlkniswwlkn  30265  el2wlkonotlem  30306  clwlkisclwwlklem2a  30372  clwlkisclwwlklem2  30373  wrdnval  30399  clwlkfclwwlk2wrd  30438  clwlkf1clwwlklem3  30446  lply1binomsc  30737  mat1dimelbas  30750
  Copyright terms: Public domain W3C validator