Theorem feq2d 6473

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538  ⟶wf 6320

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-fn 6327  df-f 6328

This theorem is referenced by:  feq12d  6475  ffdm  6510  fsng  6876  fsn2g  6877  fsnunf2  6925  issmo2  7969  qliftf  8368  elpm2r  8407  ralxpmap  8443  axdc3lem3  9863  axdc3lem4  9864  fseq1p1m1  12976  fseq1m1p1  12977  seqf1o  13407  iswrdi  13861  wrdf  13862  wrdffz  13878  ffz0iswrd  13884  wrdnval  13888  ccatalpha  13938  swrdf  14003  swrdwrdsymb  14015  cats1un  14074  cshwf  14153  wrdlen2i  14295  wwlktovf  14311  rlimi  14862  rlimmptrcl  14956  lo1mptrcl  14970  o1mptrcl  14971  o1fsum  15160  ram0  16348  funcres  17158  curf2cl  17473  uncfcurf  17481  yonedalem4c  17519  intopsn  17856  gsumprval  17890  resmhm  17977  gsumwsubmcl  17993  gsumsgrpccat  17996  gsumccatOLD  17997  gsumwmhm  18002  frmdup1  18021  frmdup3lem  18023  isghm  18350  resghm  18366  subgga  18422  gasubg  18424  psgnunilem2  18615  sylow2blem2  18738  pj2f  18816  pj1ghm  18821  frgpupf  18891  frgpup3lem  18895  gsumval3  19020  gsummptfzcl  19082  dprdf2  19122  ablfac2  19204  isabvd  19584  abvpropd  19606  cygznlem2a  20259  frgpcyg  20265  mplasclf  20736  evlssca  20761  lply1binomsc  20936  mat1dimelbas  21076  mat2pmatbas  21331  cpmadugsumlemF  21481  cnpf2  21855  ptpjcn  22216  cnextfres1  22673  cnextfres  22674  cnmpopc  23533  pi1addf  23652  pi1xfrf  23658  pi1cof  23664  mbfmptcl  24240  iblcnlem  24392  limcres  24489  cnplimc  24490  limccnp  24494  limccnp2  24495  limcun  24498  dvidlem  24518  cpnord  24538  dvaddf  24545  dvmulf  24546  dvcmulf  24548  dvcof  24551  dvcj  24553  dvrec  24558  dvmptcl  24562  dvcnvlem  24579  dvcnv  24580  rolle  24593  cmvth  24594  mvth  24595  dvlip  24596  dvlipcn  24597  c1lip2  24601  dv11cn  24604  dvivthlem1  24611  dvivthlem2  24612  dvivth  24613  dvne0  24614  lhop1lem  24616  lhop1  24617  lhop2  24618  lhop  24619  dvcnvrelem2  24621  taylthlem1  24968  taylthlem2  24969  ulmf2  24979  ulm2  24980  ulmdv  24998  pserdv  25024  rlimcxp  25559  o1cxp  25560  dchrptlem2  25849  axlowdimlem5  26740  axlowdimlem7  26742  axlowdimlem10  26745  uhgrn0  26860  wrdupgr  26878  upgrfn  26880  wrdumgr  26890  umgrfn  26892  upgr2wlk  27458  wlkres  27460  redwlklem  27461  wlkdlem1  27472  uhgrwkspthlem2  27543  usgr2wlkneq  27545  usgr2pthlem  27552  usgr2pth  27553  crctcshwlkn0  27607  wlkiswwlks2lem3  27657  wlkiswwlks2  27661  wlkiswwlksupgr2  27663  wlknewwlksn  27673  wpthswwlks2on  27747  clwlkclwwlklem2a  27783  clwlkclwwlklem1  27784  1wlkdlem1  27922  upgr3v3e3cycl  27965  upgr4cycl4dv4e  27970  isgrpo  28280  vciOLD  28344  isvclem  28360  isnvlem  28393  ajfval  28592  acunirnmpt2  30423  acunirnmpt2f  30424  wrdfd  30638  elrspunidl  31014  lbsdiflsp0  31110  smatrcl  31149  locfinref  31194  1stmbfm  31628  2ndmbfm  31629  sibfof  31708  rrvf2  31816  signshf  31968  reprsuc  31996  pfxwlk  32483  revwlk  32484  cvmliftmolem1  32641  cvmliftlem7  32651  cvmliftlem10  32654  cvmlift2lem9  32671  filnetlem4  33842  poimirlem16  35073  poimirlem19  35076  poimirlem23  35080  poimirlem24  35081  poimirlem25  35082  poimirlem29  35086  poimirlem31  35088  sdclem2  35180  sdclem1  35181  sdc  35182  fdc  35183  sstotbnd2  35212  elghomlem1OLD  35323  rngosn3  35362  frlmfzowrdb  39438  amgm4d  40906  mnurnd  40991  mptelpm  41800  fsneqrn  41840  cncfuni  42528  cncfiooicclem1  42535  dvsubf  42556  dvdivf  42564  dvbdfbdioolem1  42570  ioodvbdlimc1lem1  42573  ioodvbdlimc1lem2  42574  ioodvbdlimc1  42575  ioodvbdlimc2lem  42576  ioodvbdlimc2  42577  dvnprodlem3  42590  itgsubsticclem  42617  fourierdlem48  42796  fourierdlem49  42797  fourierdlem58  42806  fourierdlem59  42807  fourierdlem60  42808  fourierdlem61  42809  fourierdlem69  42817  fourierdlem75  42823  fourierdlem81  42829  fourierdlem89  42837  fourierdlem91  42839  fourierdlem97  42845  fourierdlem113  42861  meaf  43092  ismeannd  43106  psmeasure  43110  omef  43135  isomennd  43170  hoidmvlelem2  43235  hoidmvlelem3  43236  ovnhoi  43242  hspmbllem2  43266  sssmf  43372  smfpimioompt  43418  smffmpt  43436  2ffzoeq  43885  fundcmpsurbijinjpreimafv  43924  fargshiftf  43957  resmgmhm  44418  elbigolo1  44971  naryfvalelwrdf  45047  0aryfvalel  45048