Theorem feq2d 6715

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-fn 6561  df-f 6562

This theorem is used by:  feq2dd  6717  feq12d  6719  fco  6756  ffdm  6761  fsng  7162  fsn2g  7163  fsnunf2  7214  issmo2  8385  qliftf  8854  elpm2r  8893  ralxpmap  8952  axdc3lem3  10557  axdc3lem4  10558  fseq1p1m1  13759  fseq1m1p1  13760  seqf1o  14213  iswrdi  14689  wrdf  14690  wrdfd  14691  wrdffz  14707  ffz0iswrd  14713  wrdnval  14717  ccatalpha  14767  swrdf  14826  swrdwrdsymb  14840  cats1un  14898  cshwf  14979  wrdlen2i  15122  wwlktovf  15138  rlimi  15709  rlimmptrcl  15804  lo1mptrcl  15818  o1mptrcl  15819  o1fsum  16009  ram0  17229  funcres  18100  curf2cl  18434  uncfcurf  18442  yonedalem4c  18480  intopsn  18861  gsumprval  18906  resmgmhm  18929  resmhm  19045  gsumwsubmcl  19062  gsumsgrpccat  19065  gsumwmhm  19070  frmdup1  19089  frmdup3lem  19091  resghm  19475  subgga  19544  gasubg  19546  psgnunilem2  19739  sylow2blem2  19865  pj2f  19942  pj1ghm  19947  frgpupf  20017  frgpup3lem  20021  gsumval3  20151  gsummptfzcl  20213  dprdf2  20253  ablfac2  20335  isabvd  21099  abvpropd  21122  cygznlem2a  21903  frgpcyg  21909  psrasclcl  22317  mplasclf  22404  evlssca  22433  lply1binomsc  22659  mat1dimelbas  22816  mat2pmatbas  23074  cpmadugsumlemF  23224  cnpf2  23598  ptpjcn  23960  cnextfres1  24417  cnextfres  24418  cnmpopc  25279  pi1addf  25398  pi1xfrf  25404  pi1cof  25410  mbfmptcl  25987  iblcnlem  26139  limcres  26236  cnplimc  26237  limccnp  26241  limccnp2  26242  limcun  26245  dvidlem  26265  cpnord  26285  dvaddf  26292  dvmulf  26293  dvcmulf  26295  dvcof  26298  dvcj  26300  dvrec  26305  dvmptcl  26309  dvcnvlem  26326  dvcnv  26327  rolle  26340  cmvth  26341  mvth  26342  dvlip  26343  dvlipcn  26344  c1lip2  26348  dv11cn  26351  dvivthlem1  26358  dvivthlem2  26359  dvivth  26360  dvne0  26361  lhop1lem  26363  lhop1  26364  lhop2  26365  lhop  26366  dvcnvrelem2  26368  taylthlem1  26730  taylthlem2  26731  ulmf2  26741  ulm2  26742  ulmdv  26760  pserdv  26786  rlimcxp  27331  o1cxp  27332  dchrptlem2  27622  axlowdimlem5  29554  axlowdimlem7  29556  axlowdimlem10  29559  uhgrn0  29675  wrdupgr  29693  upgrfn  29695  wrdumgr  29705  umgrfn  29707  upgr2wlk  30277  wlkres  30279  redwlklem  30280  wlkdlem1  30291  pfxwlk  30296  revwlk  30297  uhgrwkspthlem2  30370  usgr2wlkneq  30372  usgr2pthlem  30379  usgr2pth  30380  crctcshwlkn0  30440  wlkiswwlks2lem3  30490  wlkiswwlks2  30494  wlkiswwlksupgr2  30496  wlknewwlksn  30506  wpthswwlks2on  30583  clwlkclwwlklem2a  30619  clwlkclwwlklem1  30620  1wlkdlem1  30758  upgr3v3e3cycl  30811  upgr4cycl4dv4e  30816  isgrpo  31129  vciOLD  31193  isvclem  31209  isnvlem  31242  ajfval  31441  lbsdiflsp0  34328  smatrcl  34498  locfinref  34543  1stmbfm  34962  2ndmbfm  34963  sibfof  35042  rrvf2  35150  signshf  35287  reprsuc  35314  cvmliftmolem1  36213  cvmliftlem7  36223  cvmliftlem10  36226  cvmlift2lem9  36243  filnetlem4  37347  poimirlem16  38746  poimirlem19  38749  poimirlem23  38753  poimirlem24  38754  poimirlem25  38755  poimirlem29  38759  poimirlem31  38761  sdclem2  38868  sdclem1  38869  sdc  38870  fdc  38871  sstotbnd2  38900  elghomlem1OLD  39011  rngosn3  39050  sticksstones9  43396  sticksstones11  43398  sticksstones16  43404  frlmfzowrdb  43764  evlselv  43810  ofoafg  44548  amgm4d  45392  mnurnd  45459  mptelpm  46396  fsneqrn  46429  cncfiooicclem1  47108  dvsubf  47129  dvdivf  47137  dvbdfbdioolem1  47143  ioodvbdlimc1lem1  47146  ioodvbdlimc1lem2  47147  ioodvbdlimc1  47148  ioodvbdlimc2lem  47149  ioodvbdlimc2  47150  dvnprodlem3  47163  itgsubsticclem  47190  fourierdlem58  47379  fourierdlem59  47380  fourierdlem60  47381  fourierdlem61  47382  fourierdlem69  47390  fourierdlem75  47396  fourierdlem81  47402  fourierdlem89  47410  fourierdlem91  47412  fourierdlem97  47418  meaf  47668  ismeannd  47682  psmeasure  47686  omef  47711  isomennd  47746  hoidmvlelem2  47811  hoidmvlelem3  47812  ovnhoi  47818  hspmbllem2  47842  smfpimioompt  48001  smffmptf  48019  chnsubseqword  48093  2ffzoeq  48603  fundcmpsurbijinjpreimafv  48694  fargshiftf  48727  upgrimwlklem2  49201  upgrimwlklem4  49203  upgrimpths  49212  gpgprismgr4cycllem9  49406  elbigolo1  49874  naryfvalelwrdf  49950  0aryfvalel  49951  0funcg2  50404  termcfuncval  50872