Theorem feq2d 6692

Description: Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypothesis

Ref	Expression
feq2d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
feq2d	⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))

Proof of Theorem feq2d

Step	Hyp	Ref	Expression
1		feq2d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		feq2 6687	. 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ⟶wf 6527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-fn 6534  df-f 6535

This theorem is referenced by:  feq12d  6694  fco  6730  ffdm  6735  fsng  7127  fsn2g  7128  fsnunf2  7178  issmo2  8363  qliftf  8819  elpm2r  8859  ralxpmap  8910  axdc3lem3  10466  axdc3lem4  10467  fseq1p1m1  13615  fseq1m1p1  13616  seqf1o  14061  iswrdi  14535  wrdf  14536  wrdfd  14537  wrdffz  14553  ffz0iswrd  14559  wrdnval  14563  ccatalpha  14611  swrdf  14668  swrdwrdsymb  14680  cats1un  14739  cshwf  14818  wrdlen2i  14961  wwlktovf  14975  rlimi  15529  rlimmptrcl  15624  lo1mptrcl  15638  o1mptrcl  15639  o1fsum  15829  ram0  17042  funcres  17909  curf2cl  18243  uncfcurf  18251  yonedalem4c  18289  intopsn  18632  gsumprval  18666  resmgmhm  18689  resmhm  18798  gsumwsubmcl  18815  gsumsgrpccat  18818  gsumwmhm  18823  frmdup1  18842  frmdup3lem  18844  isghmOLD  19199  resghm  19215  subgga  19283  gasubg  19285  psgnunilem2  19476  sylow2blem2  19602  pj2f  19679  pj1ghm  19684  frgpupf  19754  frgpup3lem  19758  gsumval3  19888  gsummptfzcl  19950  dprdf2  19990  ablfac2  20072  isabvd  20772  abvpropd  20795  cygznlem2a  21528  frgpcyg  21534  psrasclcl  21940  mplasclf  22023  evlssca  22047  lply1binomsc  22249  mat1dimelbas  22409  mat2pmatbas  22664  cpmadugsumlemF  22814  cnpf2  23188  ptpjcn  23549  cnextfres1  24006  cnextfres  24007  cnmpopc  24873  pi1addf  24998  pi1xfrf  25004  pi1cof  25010  mbfmptcl  25589  iblcnlem  25742  limcres  25839  cnplimc  25840  limccnp  25844  limccnp2  25845  limcun  25848  dvidlem  25868  cpnord  25889  dvaddf  25897  dvmulf  25898  dvcmulf  25900  dvcof  25904  dvcj  25906  dvrec  25911  dvmptcl  25915  dvcnvlem  25932  dvcnv  25933  rolle  25946  cmvth  25947  cmvthOLD  25948  mvth  25949  dvlip  25950  dvlipcn  25951  c1lip2  25955  dv11cn  25958  dvivthlem1  25965  dvivthlem2  25966  dvivth  25967  dvne0  25968  lhop1lem  25970  lhop1  25971  lhop2  25972  lhop  25973  dvcnvrelem2  25975  taylthlem1  26333  taylthlem2  26334  taylthlem2OLD  26335  ulmf2  26345  ulm2  26346  ulmdv  26364  pserdv  26391  rlimcxp  26936  o1cxp  26937  dchrptlem2  27228  axlowdimlem5  28925  axlowdimlem7  28927  axlowdimlem10  28930  uhgrn0  29046  wrdupgr  29064  upgrfn  29066  wrdumgr  29076  umgrfn  29078  upgr2wlk  29648  wlkres  29650  redwlklem  29651  wlkdlem1  29662  uhgrwkspthlem2  29736  usgr2wlkneq  29738  usgr2pthlem  29745  usgr2pth  29746  crctcshwlkn0  29803  wlkiswwlks2lem3  29853  wlkiswwlks2  29857  wlkiswwlksupgr2  29859  wlknewwlksn  29869  wpthswwlks2on  29943  clwlkclwwlklem2a  29979  clwlkclwwlklem1  29980  1wlkdlem1  30118  upgr3v3e3cycl  30161  upgr4cycl4dv4e  30166  isgrpo  30478  vciOLD  30542  isvclem  30558  isnvlem  30591  ajfval  30790  feq2dd  32600  acunirnmpt2  32638  acunirnmpt2f  32639  elrspunidl  33443  lbsdiflsp0  33666  smatrcl  33827  locfinref  33872  1stmbfm  34292  2ndmbfm  34293  sibfof  34372  rrvf2  34480  signshf  34620  reprsuc  34647  pfxwlk  35146  revwlk  35147  cvmliftmolem1  35303  cvmliftlem7  35313  cvmliftlem10  35316  cvmlift2lem9  35333  filnetlem4  36399  poimirlem16  37660  poimirlem19  37663  poimirlem23  37667  poimirlem24  37668  poimirlem25  37669  poimirlem29  37673  poimirlem31  37675  sdclem2  37766  sdclem1  37767  sdc  37768  fdc  37769  sstotbnd2  37798  elghomlem1OLD  37909  rngosn3  37948  sticksstones9  42167  sticksstones11  42169  sticksstones16  42175  frlmfzowrdb  42527  evlselvlem  42609  evlselv  42610  ofoafg  43378  amgm4d  44224  mnurnd  44307  mptelpm  45200  fsneqrn  45235  cncfuni  45915  cncfiooicclem1  45922  dvsubf  45943  dvdivf  45951  dvbdfbdioolem1  45957  ioodvbdlimc1lem1  45960  ioodvbdlimc1lem2  45961  ioodvbdlimc1  45962  ioodvbdlimc2lem  45963  ioodvbdlimc2  45964  dvnprodlem3  45977  itgsubsticclem  46004  fourierdlem48  46183  fourierdlem49  46184  fourierdlem58  46193  fourierdlem59  46194  fourierdlem60  46195  fourierdlem61  46196  fourierdlem69  46204  fourierdlem75  46210  fourierdlem81  46216  fourierdlem89  46224  fourierdlem91  46226  fourierdlem97  46232  fourierdlem113  46248  meaf  46482  ismeannd  46496  psmeasure  46500  omef  46525  isomennd  46560  hoidmvlelem2  46625  hoidmvlelem3  46626  ovnhoi  46632  hspmbllem2  46656  sssmf  46767  smfpimioompt  46815  smffmptf  46833  2ffzoeq  47356  fundcmpsurbijinjpreimafv  47421  fargshiftf  47454  upgrimwlklem2  47911  upgrimwlklem4  47913  upgrimpths  47922  gpgprismgr4cycllem9  48102  elbigolo1  48537  naryfvalelwrdf  48613  0aryfvalel  48614  0funcg2  49049  termcfuncval  49417