Theorem feq2d 6031

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

Step	Hyp	Ref	Expression
1		feq2d.1	. 2 |- ( ph -> A = B )
2		feq2 6027	. 2 |- ( A = B -> ( F : A --> C <-> F : B --> C ) )
3	1, 2	syl 17	1 |- ( ph -> ( F : A --> C <-> F : B --> C ) )

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   -->wf 5884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-fn 5891  df-f 5892

This theorem is referenced by:  feq12d  6033  ffdm  6062  fsng  6404  fsn2g  6405  fsnunf2  6452  issmo2  7446  qliftf  7835  elpm2r  7875  ralxpmap  7907  ordtypelem5  8427  axdc3lem3  9274  axdc3lem4  9275  fseq1p1m1  12414  fseq1m1p1  12415  seqf1o  12842  iswrdi  13309  wrdf  13310  wrdffz  13326  ffz0iswrd  13332  wrdnval  13335  ccatalpha  13375  swrdf  13425  swrd0f  13427  cats1un  13475  cshwf  13546  wrdlen2i  13686  wwlktovf  13699  rlimi  14244  rlimmptrcl  14338  lo1mptrcl  14352  o1mptrcl  14353  o1fsum  14545  ram0  15726  funcres  16556  curf2cl  16871  uncfcurf  16879  yonedalem4c  16917  intopsn  17253  gsumprval  17281  resmhm  17359  gsumwsubmcl  17375  gsumccat  17378  gsumwmhm  17382  frmdup1  17401  frmdup3lem  17403  isghm  17660  resghm  17676  subgga  17733  gasubg  17735  psgnunilem2  17915  sylow2blem2  18036  pj2f  18111  pj1ghm  18116  frgpupf  18186  frgpup3lem  18190  gsumval3  18308  gsummptfzcl  18368  dprdf2  18406  ablfaclem2  18485  ablfac2  18488  isabvd  18820  abvpropd  18842  mplasclf  19497  evlssca  19522  lply1binomsc  19677  cygznlem2a  19916  frgpcyg  19922  mat1dimelbas  20277  mat2pmatbas  20531  cpmadugsumlemF  20681  cnpf2  21054  lmcnp  21108  ptpjcn  21414  cnextfres1  21872  cnextfres  21873  cnmpt2pc  22727  pi1addf  22847  pi1xfrf  22853  pi1cof  22859  mbfmptcl  23404  iblcnlem  23555  limcres  23650  cnplimc  23651  limccnp  23655  limccnp2  23656  limcun  23659  dvidlem  23679  cpnord  23698  dvaddf  23705  dvmulf  23706  dvcmulf  23708  dvcof  23711  dvcj  23713  dvrec  23718  dvmptcl  23722  dvcnvlem  23739  dvcnv  23740  rolle  23753  cmvth  23754  mvth  23755  dvlip  23756  dvlipcn  23757  c1lip2  23761  dv11cn  23764  dvivthlem1  23771  dvivthlem2  23772  dvivth  23773  dvne0  23774  lhop1lem  23776  lhop1  23777  lhop2  23778  lhop  23779  dvcnvrelem2  23781  taylthlem1  24127  taylthlem2  24128  ulmf2  24138  ulm2  24139  ulmdv  24157  pserdv  24183  rlimcxp  24700  o1cxp  24701  dchrptlem2  24990  axlowdimlem5  25826  axlowdimlem7  25828  axlowdimlem10  25831  uhgrn0  25962  wrdupgr  25980  upgrfn  25982  wrdumgr  25992  umgrfn  25994  upgr1e  26008  umgrres1  26206  upgr2wlk  26564  wlkres  26567  redwlklem  26568  wlkdlem1  26579  uhgrwkspthlem2  26650  usgr2wlkneq  26652  usgr2pthlem  26659  usgr2pth  26660  crctcshwlkn0  26713  wlkiswwlks2lem3  26757  wlkiswwlks2  26761  wlkiswwlksupgr2  26763  wlknewwlksn  26773  clwlkclwwlklem2a  26899  clwlkclwwlklem1  26900  clwlksfclwwlk2wrd  26958  clwlksfclwwlk  26962  clwlksf1clwwlklem3  26967  1wlkdlem1  26997  upgr3v3e3cycl  27040  upgr4cycl4dv4e  27045  isgrpo  27351  vciOLD  27416  isvclem  27432  isnvlem  27465  ajfval  27664  acunirnmpt2  29460  acunirnmpt2f  29461  smatrcl  29862  locfinref  29908  1stmbfm  30322  2ndmbfm  30323  sibfof  30402  rrvf2  30510  signshf  30665  reprsuc  30693  cvmliftmolem1  31263  cvmliftlem7  31273  cvmliftlem10  31276  cvmlift2lem9  31293  filnetlem4  32376  poimirlem16  33425  poimirlem19  33428  poimirlem23  33432  poimirlem24  33433  poimirlem25  33434  poimirlem29  33438  poimirlem31  33440  sdclem2  33538  sdclem1  33539  sdc  33540  fdc  33541  sstotbnd2  33573  elghomlem1OLD  33684  rngosn3  33723  amgm4d  38503  mptelpm  39357  fsneqrn  39403  cncfuni  40099  cncfiooicclem1  40106  dvsubf  40128  dvdivf  40137  dvbdfbdioolem1  40143  ioodvbdlimc1lem1  40146  ioodvbdlimc1lem2  40147  ioodvbdlimc1  40148  ioodvbdlimc2lem  40149  ioodvbdlimc2  40150  dvnprodlem3  40163  itgsubsticclem  40191  fourierdlem48  40371  fourierdlem49  40372  fourierdlem58  40381  fourierdlem59  40382  fourierdlem60  40383  fourierdlem61  40384  fourierdlem69  40392  fourierdlem75  40398  fourierdlem81  40404  fourierdlem89  40412  fourierdlem91  40414  fourierdlem97  40420  fourierdlem113  40436  meaf  40670  ismeannd  40684  psmeasure  40688  omef  40710  isomennd  40745  hoidmvlelem2  40810  hoidmvlelem3  40811  ovnhoi  40817  hspmbllem2  40841  sssmf  40947  smfpimioompt  40993  smffmpt  41011  2ffzoeq  41338  fargshiftf  41376  resmgmhm  41798  elbigolo1  42351