Theorem feq2d 6675

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-fn 6517  df-f 6518

This theorem is referenced by:  feq2dd  6677  feq12d  6679  fco  6715  ffdm  6720  fsng  7112  fsn2g  7113  fsnunf2  7163  issmo2  8321  qliftf  8781  elpm2r  8821  ralxpmap  8872  axdc3lem3  10412  axdc3lem4  10413  fseq1p1m1  13566  fseq1m1p1  13567  seqf1o  14015  iswrdi  14489  wrdf  14490  wrdfd  14491  wrdffz  14507  ffz0iswrd  14513  wrdnval  14517  ccatalpha  14565  swrdf  14622  swrdwrdsymb  14634  cats1un  14693  cshwf  14772  wrdlen2i  14915  wwlktovf  14929  rlimi  15486  rlimmptrcl  15581  lo1mptrcl  15595  o1mptrcl  15596  o1fsum  15786  ram0  17000  funcres  17865  curf2cl  18199  uncfcurf  18207  yonedalem4c  18245  intopsn  18588  gsumprval  18622  resmgmhm  18645  resmhm  18754  gsumwsubmcl  18771  gsumsgrpccat  18774  gsumwmhm  18779  frmdup1  18798  frmdup3lem  18800  isghmOLD  19155  resghm  19171  subgga  19239  gasubg  19241  psgnunilem2  19432  sylow2blem2  19558  pj2f  19635  pj1ghm  19640  frgpupf  19710  frgpup3lem  19714  gsumval3  19844  gsummptfzcl  19906  dprdf2  19946  ablfac2  20028  isabvd  20728  abvpropd  20751  cygznlem2a  21484  frgpcyg  21490  psrasclcl  21896  mplasclf  21979  evlssca  22003  lply1binomsc  22205  mat1dimelbas  22365  mat2pmatbas  22620  cpmadugsumlemF  22770  cnpf2  23144  ptpjcn  23505  cnextfres1  23962  cnextfres  23963  cnmpopc  24829  pi1addf  24954  pi1xfrf  24960  pi1cof  24966  mbfmptcl  25544  iblcnlem  25697  limcres  25794  cnplimc  25795  limccnp  25799  limccnp2  25800  limcun  25803  dvidlem  25823  cpnord  25844  dvaddf  25852  dvmulf  25853  dvcmulf  25855  dvcof  25859  dvcj  25861  dvrec  25866  dvmptcl  25870  dvcnvlem  25887  dvcnv  25888  rolle  25901  cmvth  25902  cmvthOLD  25903  mvth  25904  dvlip  25905  dvlipcn  25906  c1lip2  25910  dv11cn  25913  dvivthlem1  25920  dvivthlem2  25921  dvivth  25922  dvne0  25923  lhop1lem  25925  lhop1  25926  lhop2  25927  lhop  25928  dvcnvrelem2  25930  taylthlem1  26288  taylthlem2  26289  taylthlem2OLD  26290  ulmf2  26300  ulm2  26301  ulmdv  26319  pserdv  26346  rlimcxp  26891  o1cxp  26892  dchrptlem2  27183  axlowdimlem5  28880  axlowdimlem7  28882  axlowdimlem10  28885  uhgrn0  29001  wrdupgr  29019  upgrfn  29021  wrdumgr  29031  umgrfn  29033  upgr2wlk  29603  wlkres  29605  redwlklem  29606  wlkdlem1  29617  uhgrwkspthlem2  29691  usgr2wlkneq  29693  usgr2pthlem  29700  usgr2pth  29701  crctcshwlkn0  29758  wlkiswwlks2lem3  29808  wlkiswwlks2  29812  wlkiswwlksupgr2  29814  wlknewwlksn  29824  wpthswwlks2on  29898  clwlkclwwlklem2a  29934  clwlkclwwlklem1  29935  1wlkdlem1  30073  upgr3v3e3cycl  30116  upgr4cycl4dv4e  30121  isgrpo  30433  vciOLD  30497  isvclem  30513  isnvlem  30546  ajfval  30745  acunirnmpt2  32591  acunirnmpt2f  32592  elrspunidl  33406  lbsdiflsp0  33629  smatrcl  33793  locfinref  33838  1stmbfm  34258  2ndmbfm  34259  sibfof  34338  rrvf2  34446  signshf  34586  reprsuc  34613  pfxwlk  35118  revwlk  35119  cvmliftmolem1  35275  cvmliftlem7  35285  cvmliftlem10  35288  cvmlift2lem9  35305  filnetlem4  36376  poimirlem16  37637  poimirlem19  37640  poimirlem23  37644  poimirlem24  37645  poimirlem25  37646  poimirlem29  37650  poimirlem31  37652  sdclem2  37743  sdclem1  37744  sdc  37745  fdc  37746  sstotbnd2  37775  elghomlem1OLD  37886  rngosn3  37925  sticksstones9  42149  sticksstones11  42151  sticksstones16  42157  frlmfzowrdb  42499  evlselvlem  42581  evlselv  42582  ofoafg  43350  amgm4d  44196  mnurnd  44279  mptelpm  45177  fsneqrn  45212  cncfuni  45891  cncfiooicclem1  45898  dvsubf  45919  dvdivf  45927  dvbdfbdioolem1  45933  ioodvbdlimc1lem1  45936  ioodvbdlimc1lem2  45937  ioodvbdlimc1  45938  ioodvbdlimc2lem  45939  ioodvbdlimc2  45940  dvnprodlem3  45953  itgsubsticclem  45980  fourierdlem48  46159  fourierdlem49  46160  fourierdlem58  46169  fourierdlem59  46170  fourierdlem60  46171  fourierdlem61  46172  fourierdlem69  46180  fourierdlem75  46186  fourierdlem81  46192  fourierdlem89  46200  fourierdlem91  46202  fourierdlem97  46208  fourierdlem113  46224  meaf  46458  ismeannd  46472  psmeasure  46476  omef  46501  isomennd  46536  hoidmvlelem2  46601  hoidmvlelem3  46602  ovnhoi  46608  hspmbllem2  46632  sssmf  46743  smfpimioompt  46791  smffmptf  46809  2ffzoeq  47332  fundcmpsurbijinjpreimafv  47412  fargshiftf  47445  upgrimwlklem2  47902  upgrimwlklem4  47904  upgrimpths  47913  gpgprismgr4cycllem9  48097  elbigolo1  48550  naryfvalelwrdf  48626  0aryfvalel  48627  0funcg2  49077  termcfuncval  49525