Theorem feq2d 6672

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 6667	. 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))

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

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 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-fn 6514  df-f 6515

This theorem is referenced by:  feq2dd  6674  feq12d  6676  fco  6712  ffdm  6717  fsng  7109  fsn2g  7110  fsnunf2  7160  issmo2  8318  qliftf  8778  elpm2r  8818  ralxpmap  8869  axdc3lem3  10405  axdc3lem4  10406  fseq1p1m1  13559  fseq1m1p1  13560  seqf1o  14008  iswrdi  14482  wrdf  14483  wrdfd  14484  wrdffz  14500  ffz0iswrd  14506  wrdnval  14510  ccatalpha  14558  swrdf  14615  swrdwrdsymb  14627  cats1un  14686  cshwf  14765  wrdlen2i  14908  wwlktovf  14922  rlimi  15479  rlimmptrcl  15574  lo1mptrcl  15588  o1mptrcl  15589  o1fsum  15779  ram0  16993  funcres  17858  curf2cl  18192  uncfcurf  18200  yonedalem4c  18238  intopsn  18581  gsumprval  18615  resmgmhm  18638  resmhm  18747  gsumwsubmcl  18764  gsumsgrpccat  18767  gsumwmhm  18772  frmdup1  18791  frmdup3lem  18793  isghmOLD  19148  resghm  19164  subgga  19232  gasubg  19234  psgnunilem2  19425  sylow2blem2  19551  pj2f  19628  pj1ghm  19633  frgpupf  19703  frgpup3lem  19707  gsumval3  19837  gsummptfzcl  19899  dprdf2  19939  ablfac2  20021  isabvd  20721  abvpropd  20744  cygznlem2a  21477  frgpcyg  21483  psrasclcl  21889  mplasclf  21972  evlssca  21996  lply1binomsc  22198  mat1dimelbas  22358  mat2pmatbas  22613  cpmadugsumlemF  22763  cnpf2  23137  ptpjcn  23498  cnextfres1  23955  cnextfres  23956  cnmpopc  24822  pi1addf  24947  pi1xfrf  24953  pi1cof  24959  mbfmptcl  25537  iblcnlem  25690  limcres  25787  cnplimc  25788  limccnp  25792  limccnp2  25793  limcun  25796  dvidlem  25816  cpnord  25837  dvaddf  25845  dvmulf  25846  dvcmulf  25848  dvcof  25852  dvcj  25854  dvrec  25859  dvmptcl  25863  dvcnvlem  25880  dvcnv  25881  rolle  25894  cmvth  25895  cmvthOLD  25896  mvth  25897  dvlip  25898  dvlipcn  25899  c1lip2  25903  dv11cn  25906  dvivthlem1  25913  dvivthlem2  25914  dvivth  25915  dvne0  25916  lhop1lem  25918  lhop1  25919  lhop2  25920  lhop  25921  dvcnvrelem2  25923  taylthlem1  26281  taylthlem2  26282  taylthlem2OLD  26283  ulmf2  26293  ulm2  26294  ulmdv  26312  pserdv  26339  rlimcxp  26884  o1cxp  26885  dchrptlem2  27176  axlowdimlem5  28873  axlowdimlem7  28875  axlowdimlem10  28878  uhgrn0  28994  wrdupgr  29012  upgrfn  29014  wrdumgr  29024  umgrfn  29026  upgr2wlk  29596  wlkres  29598  redwlklem  29599  wlkdlem1  29610  uhgrwkspthlem2  29684  usgr2wlkneq  29686  usgr2pthlem  29693  usgr2pth  29694  crctcshwlkn0  29751  wlkiswwlks2lem3  29801  wlkiswwlks2  29805  wlkiswwlksupgr2  29807  wlknewwlksn  29817  wpthswwlks2on  29891  clwlkclwwlklem2a  29927  clwlkclwwlklem1  29928  1wlkdlem1  30066  upgr3v3e3cycl  30109  upgr4cycl4dv4e  30114  isgrpo  30426  vciOLD  30490  isvclem  30506  isnvlem  30539  ajfval  30738  acunirnmpt2  32584  acunirnmpt2f  32585  elrspunidl  33399  lbsdiflsp0  33622  smatrcl  33786  locfinref  33831  1stmbfm  34251  2ndmbfm  34252  sibfof  34331  rrvf2  34439  signshf  34579  reprsuc  34606  pfxwlk  35111  revwlk  35112  cvmliftmolem1  35268  cvmliftlem7  35278  cvmliftlem10  35281  cvmlift2lem9  35298  filnetlem4  36369  poimirlem16  37630  poimirlem19  37633  poimirlem23  37637  poimirlem24  37638  poimirlem25  37639  poimirlem29  37643  poimirlem31  37645  sdclem2  37736  sdclem1  37737  sdc  37738  fdc  37739  sstotbnd2  37768  elghomlem1OLD  37879  rngosn3  37918  sticksstones9  42142  sticksstones11  42144  sticksstones16  42150  frlmfzowrdb  42492  evlselvlem  42574  evlselv  42575  ofoafg  43343  amgm4d  44189  mnurnd  44272  mptelpm  45170  fsneqrn  45205  cncfuni  45884  cncfiooicclem1  45891  dvsubf  45912  dvdivf  45920  dvbdfbdioolem1  45926  ioodvbdlimc1lem1  45929  ioodvbdlimc1lem2  45930  ioodvbdlimc1  45931  ioodvbdlimc2lem  45932  ioodvbdlimc2  45933  dvnprodlem3  45946  itgsubsticclem  45973  fourierdlem48  46152  fourierdlem49  46153  fourierdlem58  46162  fourierdlem59  46163  fourierdlem60  46164  fourierdlem61  46165  fourierdlem69  46173  fourierdlem75  46179  fourierdlem81  46185  fourierdlem89  46193  fourierdlem91  46195  fourierdlem97  46201  fourierdlem113  46217  meaf  46451  ismeannd  46465  psmeasure  46469  omef  46494  isomennd  46529  hoidmvlelem2  46594  hoidmvlelem3  46595  ovnhoi  46601  hspmbllem2  46625  sssmf  46736  smfpimioompt  46784  smffmptf  46802  2ffzoeq  47328  fundcmpsurbijinjpreimafv  47408  fargshiftf  47441  upgrimwlklem2  47898  upgrimwlklem4  47900  upgrimpths  47909  gpgprismgr4cycllem9  48093  elbigolo1  48546  naryfvalelwrdf  48622  0aryfvalel  48623  0funcg2  49073  termcfuncval  49521