MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  feq2d Structured version   Visualization version   GIF version

Theorem feq2d 6497
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
StepHypRef Expression
1 feq2d.1 . 2 (𝜑𝐴 = 𝐵)
2 feq2 6493 . 2 (𝐴 = 𝐵 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1530  wf 6348
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-9 2117  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-cleq 2819  df-fn 6355  df-f 6356
This theorem is referenced by:  feq12d  6499  ffdm  6533  fsng  6895  fsn2g  6896  fsnunf2  6944  issmo2  7977  qliftf  8375  elpm2r  8414  ralxpmap  8449  axdc3lem3  9863  axdc3lem4  9864  fseq1p1m1  12971  fseq1m1p1  12972  seqf1o  13401  iswrdi  13855  wrdf  13856  wrdffz  13875  ffz0iswrd  13881  ffz0iswrdOLD  13882  wrdnval  13886  ccatalpha  13937  swrdf  14002  swrdwrdsymb  14014  cats1un  14073  cshwf  14152  wrdlen2i  14294  wwlktovf  14310  rlimi  14860  rlimmptrcl  14954  lo1mptrcl  14968  o1mptrcl  14969  o1fsum  15158  ram0  16348  funcres  17156  curf2cl  17471  uncfcurf  17479  yonedalem4c  17517  intopsn  17853  gsumprval  17887  resmhm  17968  gsumwsubmcl  17984  gsumsgrpccat  17987  gsumccatOLD  17988  gsumwmhm  17993  frmdup1  18012  frmdup3lem  18014  isghm  18288  resghm  18304  subgga  18360  gasubg  18362  psgnunilem2  18543  sylow2blem2  18666  pj2f  18744  pj1ghm  18749  frgpupf  18819  frgpup3lem  18823  gsumval3  18947  gsummptfzcl  19009  dprdf2  19049  ablfac2  19131  isabvd  19511  abvpropd  19533  mplasclf  20196  evlssca  20221  lply1binomsc  20394  cygznlem2a  20633  frgpcyg  20639  mat1dimelbas  20999  mat2pmatbas  21253  cpmadugsumlemF  21403  cnpf2  21777  ptpjcn  22138  cnextfres1  22595  cnextfres  22596  cnmpopc  23450  pi1addf  23569  pi1xfrf  23575  pi1cof  23581  mbfmptcl  24155  iblcnlem  24307  limcres  24402  cnplimc  24403  limccnp  24407  limccnp2  24408  limcun  24411  dvidlem  24431  cpnord  24450  dvaddf  24457  dvmulf  24458  dvcmulf  24460  dvcof  24463  dvcj  24465  dvrec  24470  dvmptcl  24474  dvcnvlem  24491  dvcnv  24492  rolle  24505  cmvth  24506  mvth  24507  dvlip  24508  dvlipcn  24509  c1lip2  24513  dv11cn  24516  dvivthlem1  24523  dvivthlem2  24524  dvivth  24525  dvne0  24526  lhop1lem  24528  lhop1  24529  lhop2  24530  lhop  24531  dvcnvrelem2  24533  taylthlem1  24879  taylthlem2  24880  ulmf2  24890  ulm2  24891  ulmdv  24909  pserdv  24935  rlimcxp  25468  o1cxp  25469  dchrptlem2  25758  axlowdimlem5  26649  axlowdimlem7  26651  axlowdimlem10  26654  uhgrn0  26769  wrdupgr  26787  upgrfn  26789  wrdumgr  26799  umgrfn  26801  upgr2wlk  27367  wlkres  27369  redwlklem  27370  wlkdlem1  27381  uhgrwkspthlem2  27452  usgr2wlkneq  27454  usgr2pthlem  27461  usgr2pth  27462  crctcshwlkn0  27516  wlkiswwlks2lem3  27566  wlkiswwlks2  27570  wlkiswwlksupgr2  27572  wlknewwlksn  27582  wpthswwlks2on  27657  clwlkclwwlklem2a  27693  clwlkclwwlklem1  27694  1wlkdlem1  27833  upgr3v3e3cycl  27876  upgr4cycl4dv4e  27881  isgrpo  28191  vciOLD  28255  isvclem  28271  isnvlem  28304  ajfval  28503  acunirnmpt2  30323  acunirnmpt2f  30324  wrdfd  30529  lbsdiflsp0  30911  smatrcl  30950  locfinref  30994  1stmbfm  31407  2ndmbfm  31408  sibfof  31487  rrvf2  31595  signshf  31747  reprsuc  31775  pfxwlk  32257  revwlk  32258  cvmliftmolem1  32415  cvmliftlem7  32425  cvmliftlem10  32428  cvmlift2lem9  32445  filnetlem4  33616  poimirlem16  34778  poimirlem19  34781  poimirlem23  34785  poimirlem24  34786  poimirlem25  34787  poimirlem29  34791  poimirlem31  34793  sdclem2  34888  sdclem1  34889  sdc  34890  fdc  34891  sstotbnd2  34923  elghomlem1OLD  35034  rngosn3  35073  frlmfzowrdb  39011  amgm4d  40422  mnurnd  40487  mptelpm  41300  fsneqrn  41342  cncfuni  42037  cncfiooicclem1  42044  dvsubf  42066  dvdivf  42075  dvbdfbdioolem1  42081  ioodvbdlimc1lem1  42084  ioodvbdlimc1lem2  42085  ioodvbdlimc1  42086  ioodvbdlimc2lem  42087  ioodvbdlimc2  42088  dvnprodlem3  42101  itgsubsticclem  42128  fourierdlem48  42308  fourierdlem49  42309  fourierdlem58  42318  fourierdlem59  42319  fourierdlem60  42320  fourierdlem61  42321  fourierdlem69  42329  fourierdlem75  42335  fourierdlem81  42341  fourierdlem89  42349  fourierdlem91  42351  fourierdlem97  42357  fourierdlem113  42373  meaf  42604  ismeannd  42618  psmeasure  42622  omef  42647  isomennd  42682  hoidmvlelem2  42747  hoidmvlelem3  42748  ovnhoi  42754  hspmbllem2  42778  sssmf  42884  smfpimioompt  42930  smffmpt  42948  2ffzoeq  43397  fargshiftf  43435  resmgmhm  43900  elbigolo1  44452
  Copyright terms: Public domain W3C validator