Theorem feq2d 6595

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ⟶wf 6433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-fn 6440  df-f 6441

This theorem is referenced by:  feq12d  6597  fco  6633  ffdm  6639  fsng  7018  fsn2g  7019  fsnunf2  7067  issmo2  8189  qliftf  8603  elpm2r  8642  ralxpmap  8693  axdc3lem3  10217  axdc3lem4  10218  fseq1p1m1  13339  fseq1m1p1  13340  seqf1o  13773  iswrdi  14230  wrdf  14231  wrdffz  14247  ffz0iswrd  14253  wrdnval  14257  ccatalpha  14307  swrdf  14372  swrdwrdsymb  14384  cats1un  14443  cshwf  14522  wrdlen2i  14664  wwlktovf  14680  rlimi  15231  rlimmptrcl  15326  lo1mptrcl  15340  o1mptrcl  15341  o1fsum  15534  ram0  16732  funcres  17620  curf2cl  17958  uncfcurf  17966  yonedalem4c  18004  intopsn  18347  gsumprval  18381  resmhm  18468  gsumwsubmcl  18484  gsumsgrpccat  18487  gsumccatOLD  18488  gsumwmhm  18493  frmdup1  18512  frmdup3lem  18514  isghm  18843  resghm  18859  subgga  18915  gasubg  18917  psgnunilem2  19112  sylow2blem2  19235  pj2f  19313  pj1ghm  19318  frgpupf  19388  frgpup3lem  19392  gsumval3  19517  gsummptfzcl  19579  dprdf2  19619  ablfac2  19701  isabvd  20089  abvpropd  20111  cygznlem2a  20784  frgpcyg  20790  mplasclf  21282  evlssca  21308  lply1binomsc  21487  mat1dimelbas  21629  mat2pmatbas  21884  cpmadugsumlemF  22034  cnpf2  22410  ptpjcn  22771  cnextfres1  23228  cnextfres  23229  cnmpopc  24100  pi1addf  24219  pi1xfrf  24225  pi1cof  24231  mbfmptcl  24809  iblcnlem  24962  limcres  25059  cnplimc  25060  limccnp  25064  limccnp2  25065  limcun  25068  dvidlem  25088  cpnord  25108  dvaddf  25115  dvmulf  25116  dvcmulf  25118  dvcof  25121  dvcj  25123  dvrec  25128  dvmptcl  25132  dvcnvlem  25149  dvcnv  25150  rolle  25163  cmvth  25164  mvth  25165  dvlip  25166  dvlipcn  25167  c1lip2  25171  dv11cn  25174  dvivthlem1  25181  dvivthlem2  25182  dvivth  25183  dvne0  25184  lhop1lem  25186  lhop1  25187  lhop2  25188  lhop  25189  dvcnvrelem2  25191  taylthlem1  25541  taylthlem2  25542  ulmf2  25552  ulm2  25553  ulmdv  25571  pserdv  25597  rlimcxp  26132  o1cxp  26133  dchrptlem2  26422  axlowdimlem5  27323  axlowdimlem7  27325  axlowdimlem10  27328  uhgrn0  27446  wrdupgr  27464  upgrfn  27466  wrdumgr  27476  umgrfn  27478  upgr2wlk  28045  wlkres  28047  redwlklem  28048  wlkdlem1  28059  uhgrwkspthlem2  28131  usgr2wlkneq  28133  usgr2pthlem  28140  usgr2pth  28141  crctcshwlkn0  28195  wlkiswwlks2lem3  28245  wlkiswwlks2  28249  wlkiswwlksupgr2  28251  wlknewwlksn  28261  wpthswwlks2on  28335  clwlkclwwlklem2a  28371  clwlkclwwlklem1  28372  1wlkdlem1  28510  upgr3v3e3cycl  28553  upgr4cycl4dv4e  28558  isgrpo  28868  vciOLD  28932  isvclem  28948  isnvlem  28981  ajfval  29180  acunirnmpt2  31006  acunirnmpt2f  31007  wrdfd  31219  elrspunidl  31615  lbsdiflsp0  31716  smatrcl  31755  locfinref  31800  1stmbfm  32236  2ndmbfm  32237  sibfof  32316  rrvf2  32424  signshf  32576  reprsuc  32604  pfxwlk  33094  revwlk  33095  cvmliftmolem1  33252  cvmliftlem7  33262  cvmliftlem10  33265  cvmlift2lem9  33282  filnetlem4  34579  poimirlem16  35802  poimirlem19  35805  poimirlem23  35809  poimirlem24  35810  poimirlem25  35811  poimirlem29  35815  poimirlem31  35817  sdclem2  35909  sdclem1  35910  sdc  35911  fdc  35912  sstotbnd2  35941  elghomlem1OLD  36052  rngosn3  36091  sticksstones9  40117  sticksstones11  40119  sticksstones16  40125  frlmfzowrdb  40242  amgm4d  41818  mnurnd  41908  mptelpm  42719  fsneqrn  42758  cncfuni  43434  cncfiooicclem1  43441  dvsubf  43462  dvdivf  43470  dvbdfbdioolem1  43476  ioodvbdlimc1lem1  43479  ioodvbdlimc1lem2  43480  ioodvbdlimc1  43481  ioodvbdlimc2lem  43482  ioodvbdlimc2  43483  dvnprodlem3  43496  itgsubsticclem  43523  fourierdlem48  43702  fourierdlem49  43703  fourierdlem58  43712  fourierdlem59  43713  fourierdlem60  43714  fourierdlem61  43715  fourierdlem69  43723  fourierdlem75  43729  fourierdlem81  43735  fourierdlem89  43743  fourierdlem91  43745  fourierdlem97  43751  fourierdlem113  43767  meaf  43998  ismeannd  44012  psmeasure  44016  omef  44041  isomennd  44076  hoidmvlelem2  44141  hoidmvlelem3  44142  ovnhoi  44148  hspmbllem2  44172  sssmf  44283  smfpimioompt  44331  smffmpt  44349  2ffzoeq  44831  fundcmpsurbijinjpreimafv  44870  fargshiftf  44903  resmgmhm  45363  elbigolo1  45914  naryfvalelwrdf  45990  0aryfvalel  45991