Theorem feq2d 6690

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ⟶wf 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-fn 6540  df-f 6541

This theorem is used by:  feq2dd  6692  feq12d  6694  fco  6731  ffdm  6736  fsng  7135  fsn2g  7136  fsnunf2  7188  issmo2  8342  qliftf  8809  elpm2r  8848  ralxpmap  8907  axdc3lem3  10458  axdc3lem4  10459  fseq1p1m1  13657  fseq1m1p1  13658  seqf1o  14111  iswrdi  14586  wrdf  14587  wrdfd  14588  wrdffz  14604  ffz0iswrd  14610  wrdnval  14614  ccatalpha  14664  swrdf  14722  swrdwrdsymb  14736  cats1un  14794  cshwf  14875  wrdlen2i  15017  wwlktovf  15033  rlimi  15604  rlimmptrcl  15699  lo1mptrcl  15713  o1mptrcl  15714  o1fsum  15904  ram0  17120  funcres  17991  curf2cl  18325  uncfcurf  18333  yonedalem4c  18371  intopsn  18752  gsumprval  18796  resmgmhm  18819  resmhm  18935  gsumwsubmcl  18952  gsumsgrpccat  18955  gsumwmhm  18960  frmdup1  18979  frmdup3lem  18981  resghm  19365  subgga  19433  gasubg  19435  psgnunilem2  19628  sylow2blem2  19754  pj2f  19831  pj1ghm  19836  frgpupf  19906  frgpup3lem  19910  gsumval3  20040  gsummptfzcl  20102  dprdf2  20142  ablfac2  20224  isabvd  20984  abvpropd  21007  cygznlem2a  21786  frgpcyg  21792  psrasclcl  22200  mplasclf  22287  evlssca  22316  lply1binomsc  22542  mat1dimelbas  22699  mat2pmatbas  22957  cpmadugsumlemF  23107  cnpf2  23481  ptpjcn  23843  cnextfres1  24300  cnextfres  24301  cnmpopc  25162  pi1addf  25281  pi1xfrf  25287  pi1cof  25293  mbfmptcl  25870  iblcnlem  26023  limcres  26120  cnplimc  26121  limccnp  26125  limccnp2  26126  limcun  26129  dvidlem  26149  cpnord  26169  dvaddf  26176  dvmulf  26177  dvcmulf  26179  dvcof  26182  dvcj  26184  dvrec  26189  dvmptcl  26193  dvcnvlem  26210  dvcnv  26211  rolle  26224  cmvth  26225  mvth  26226  dvlip  26227  dvlipcn  26228  c1lip2  26232  dv11cn  26235  dvivthlem1  26242  dvivthlem2  26243  dvivth  26244  dvne0  26245  lhop1lem  26247  lhop1  26248  lhop2  26249  lhop  26250  dvcnvrelem2  26252  taylthlem1  26616  taylthlem2  26617  ulmf2  26627  ulm2  26628  ulmdv  26646  pserdv  26672  rlimcxp  27218  o1cxp  27219  dchrptlem2  27509  axlowdimlem5  29411  axlowdimlem7  29413  axlowdimlem10  29416  uhgrn0  29532  wrdupgr  29550  upgrfn  29552  wrdumgr  29562  umgrfn  29564  upgr2wlk  30134  wlkres  30136  redwlklem  30137  wlkdlem1  30148  pfxwlk  30153  revwlk  30154  uhgrwkspthlem2  30227  usgr2wlkneq  30229  usgr2pthlem  30236  usgr2pth  30237  crctcshwlkn0  30297  wlkiswwlks2lem3  30347  wlkiswwlks2  30351  wlkiswwlksupgr2  30353  wlknewwlksn  30363  wpthswwlks2on  30440  clwlkclwwlklem2a  30476  clwlkclwwlklem1  30477  1wlkdlem1  30615  upgr3v3e3cycl  30668  upgr4cycl4dv4e  30673  isgrpo  30986  vciOLD  31050  isvclem  31066  isnvlem  31099  ajfval  31298  acunirnmpt2  33141  acunirnmpt2f  33142  elrspunidl  33864  lbsdiflsp0  34144  smatrcl  34314  locfinref  34359  1stmbfm  34779  2ndmbfm  34780  sibfof  34859  rrvf2  34967  signshf  35104  reprsuc  35131  cvmliftmolem1  35868  cvmliftlem7  35878  cvmliftlem10  35881  cvmlift2lem9  35898  filnetlem4  37008  poimirlem16  38393  poimirlem19  38396  poimirlem23  38400  poimirlem24  38401  poimirlem25  38402  poimirlem29  38406  poimirlem31  38408  sdclem2  38500  sdclem1  38501  sdc  38502  fdc  38503  sstotbnd2  38532  elghomlem1OLD  38643  rngosn3  38682  sticksstones9  43028  sticksstones11  43030  sticksstones16  43036  frlmfzowrdb  43400  evlselv  43443  ofoafg  44203  amgm4d  45048  mnurnd  45115  mptelpm  46016  fsneqrn  46049  cncfiooicclem1  46729  dvsubf  46750  dvdivf  46758  dvbdfbdioolem1  46764  ioodvbdlimc1lem1  46767  ioodvbdlimc1lem2  46768  ioodvbdlimc1  46769  ioodvbdlimc2lem  46770  ioodvbdlimc2  46771  dvnprodlem3  46784  itgsubsticclem  46811  fourierdlem58  47000  fourierdlem59  47001  fourierdlem60  47002  fourierdlem61  47003  fourierdlem69  47011  fourierdlem75  47017  fourierdlem81  47023  fourierdlem89  47031  fourierdlem91  47033  fourierdlem97  47039  meaf  47289  ismeannd  47303  psmeasure  47307  omef  47332  isomennd  47367  hoidmvlelem2  47432  hoidmvlelem3  47433  ovnhoi  47439  hspmbllem2  47463  smfpimioompt  47622  smffmptf  47640  chnsubseqword  47714  2ffzoeq  48224  fundcmpsurbijinjpreimafv  48315  fargshiftf  48348  upgrimwlklem2  48822  upgrimwlklem4  48824  upgrimpths  48833  gpgprismgr4cycllem9  49027  elbigolo1  49495  naryfvalelwrdf  49571  0aryfvalel  49572  0funcg2  50018  termcfuncval  50466