Theorem feq2d 6704

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542  ⟶wf 6540

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-fn 6547  df-f 6548

This theorem is referenced by:  feq12d  6706  fco  6742  ffdm  6748  fsng  7135  fsn2g  7136  fsnunf2  7184  issmo2  8349  qliftf  8799  elpm2r  8839  ralxpmap  8890  axdc3lem3  10447  axdc3lem4  10448  fseq1p1m1  13575  fseq1m1p1  13576  seqf1o  14009  iswrdi  14468  wrdf  14469  wrdffz  14485  ffz0iswrd  14491  wrdnval  14495  ccatalpha  14543  swrdf  14600  swrdwrdsymb  14612  cats1un  14671  cshwf  14750  wrdlen2i  14893  wwlktovf  14907  rlimi  15457  rlimmptrcl  15552  lo1mptrcl  15566  o1mptrcl  15567  o1fsum  15759  ram0  16955  funcres  17846  curf2cl  18184  uncfcurf  18192  yonedalem4c  18230  intopsn  18573  gsumprval  18607  resmhm  18701  gsumwsubmcl  18718  gsumsgrpccat  18721  gsumwmhm  18726  frmdup1  18745  frmdup3lem  18747  isghm  19092  resghm  19108  subgga  19164  gasubg  19166  psgnunilem2  19363  sylow2blem2  19489  pj2f  19566  pj1ghm  19571  frgpupf  19641  frgpup3lem  19645  gsumval3  19775  gsummptfzcl  19837  dprdf2  19877  ablfac2  19959  isabvd  20428  abvpropd  20450  cygznlem2a  21123  frgpcyg  21129  mplasclf  21626  evlssca  21652  lply1binomsc  21831  mat1dimelbas  21973  mat2pmatbas  22228  cpmadugsumlemF  22378  cnpf2  22754  ptpjcn  23115  cnextfres1  23572  cnextfres  23573  cnmpopc  24444  pi1addf  24563  pi1xfrf  24569  pi1cof  24575  mbfmptcl  25153  iblcnlem  25306  limcres  25403  cnplimc  25404  limccnp  25408  limccnp2  25409  limcun  25412  dvidlem  25432  cpnord  25452  dvaddf  25459  dvmulf  25460  dvcmulf  25462  dvcof  25465  dvcj  25467  dvrec  25472  dvmptcl  25476  dvcnvlem  25493  dvcnv  25494  rolle  25507  cmvth  25508  mvth  25509  dvlip  25510  dvlipcn  25511  c1lip2  25515  dv11cn  25518  dvivthlem1  25525  dvivthlem2  25526  dvivth  25527  dvne0  25528  lhop1lem  25530  lhop1  25531  lhop2  25532  lhop  25533  dvcnvrelem2  25535  taylthlem1  25885  taylthlem2  25886  ulmf2  25896  ulm2  25897  ulmdv  25915  pserdv  25941  rlimcxp  26478  o1cxp  26479  dchrptlem2  26768  axlowdimlem5  28204  axlowdimlem7  28206  axlowdimlem10  28209  uhgrn0  28327  wrdupgr  28345  upgrfn  28347  wrdumgr  28357  umgrfn  28359  upgr2wlk  28925  wlkres  28927  redwlklem  28928  wlkdlem1  28939  uhgrwkspthlem2  29011  usgr2wlkneq  29013  usgr2pthlem  29020  usgr2pth  29021  crctcshwlkn0  29075  wlkiswwlks2lem3  29125  wlkiswwlks2  29129  wlkiswwlksupgr2  29131  wlknewwlksn  29141  wpthswwlks2on  29215  clwlkclwwlklem2a  29251  clwlkclwwlklem1  29252  1wlkdlem1  29390  upgr3v3e3cycl  29433  upgr4cycl4dv4e  29438  isgrpo  29750  vciOLD  29814  isvclem  29830  isnvlem  29863  ajfval  30062  acunirnmpt2  31885  acunirnmpt2f  31886  wrdfd  32102  elrspunidl  32546  lbsdiflsp0  32711  smatrcl  32776  locfinref  32821  1stmbfm  33259  2ndmbfm  33260  sibfof  33339  rrvf2  33447  signshf  33599  reprsuc  33627  pfxwlk  34114  revwlk  34115  cvmliftmolem1  34272  cvmliftlem7  34282  cvmliftlem10  34285  cvmlift2lem9  34302  gg-cmvth  35181  filnetlem4  35266  poimirlem16  36504  poimirlem19  36507  poimirlem23  36511  poimirlem24  36512  poimirlem25  36513  poimirlem29  36517  poimirlem31  36519  sdclem2  36610  sdclem1  36611  sdc  36612  fdc  36613  sstotbnd2  36642  elghomlem1OLD  36753  rngosn3  36792  sticksstones9  40970  sticksstones11  40972  sticksstones16  40978  frlmfzowrdb  41078  evlselvlem  41158  evlselv  41159  ofoafg  42104  amgm4d  42952  mnurnd  43042  mptelpm  43872  fsneqrn  43910  cncfuni  44602  cncfiooicclem1  44609  dvsubf  44630  dvdivf  44638  dvbdfbdioolem1  44644  ioodvbdlimc1lem1  44647  ioodvbdlimc1lem2  44648  ioodvbdlimc1  44649  ioodvbdlimc2lem  44650  ioodvbdlimc2  44651  dvnprodlem3  44664  itgsubsticclem  44691  fourierdlem48  44870  fourierdlem49  44871  fourierdlem58  44880  fourierdlem59  44881  fourierdlem60  44882  fourierdlem61  44883  fourierdlem69  44891  fourierdlem75  44897  fourierdlem81  44903  fourierdlem89  44911  fourierdlem91  44913  fourierdlem97  44919  fourierdlem113  44935  meaf  45169  ismeannd  45183  psmeasure  45187  omef  45212  isomennd  45247  hoidmvlelem2  45312  hoidmvlelem3  45313  ovnhoi  45319  hspmbllem2  45343  sssmf  45454  smfpimioompt  45502  smffmptf  45520  2ffzoeq  46036  fundcmpsurbijinjpreimafv  46075  fargshiftf  46108  resmgmhm  46568  elbigolo1  47243  naryfvalelwrdf  47319  0aryfvalel  47320