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

Theorem feq2d 5944
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 5940 . 2 (𝐴 = 𝐵 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195   = wceq 1475  wf 5800
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-an 385  df-cleq 2603  df-fn 5807  df-f 5808
This theorem is referenced by:  feq12d  5946  ffdm  5975  fsng  6310  fsn2g  6311  fsnunf2  6357  issmo2  7333  qliftf  7722  elpm2r  7761  ralxpmap  7793  ordtypelem5  8310  axdc3lem3  9157  axdc3lem4  9158  fseq1p1m1  12283  fseq1m1p1  12284  seqf1o  12704  iswrdi  13164  wrdf  13165  wrdffz  13181  ffz0iswrd  13187  wrdnval  13190  ccatalpha  13228  swrdf  13277  swrd0f  13279  cats1un  13327  cshwf  13397  wrdlen2i  13534  wwlktovf  13547  rlimi  14092  rlimmptrcl  14186  lo1mptrcl  14200  o1mptrcl  14201  o1fsum  14386  ram0  15564  funcres  16379  curf2cl  16694  uncfcurf  16702  yonedalem4c  16740  intopsn  17076  gsumprval  17104  resmhm  17182  gsumwsubmcl  17198  gsumccat  17201  gsumwmhm  17205  frmdup1  17224  frmdup3lem  17226  isghm  17483  resghm  17499  subgga  17556  gasubg  17558  psgnunilem2  17738  sylow2blem2  17859  pj2f  17934  pj1ghm  17939  frgpupf  18009  frgpup3lem  18013  gsumval3  18131  gsummptfzcl  18191  dprdf2  18229  ablfaclem2  18308  ablfac2  18311  isabvd  18643  abvpropd  18665  mplasclf  19318  evlssca  19343  lply1binomsc  19498  cygznlem2a  19735  frgpcyg  19741  mat1dimelbas  20096  mat2pmatbas  20350  cpmadugsumlemF  20500  cnpf2  20864  lmcnp  20918  ptpjcn  21224  cnextfres1  21682  cnextfres  21683  cnmpt2pc  22535  pi1addf  22655  pi1xfrf  22661  pi1cof  22667  mbfmptcl  23210  iblcnlem  23361  limcres  23456  cnplimc  23457  limccnp  23461  limccnp2  23462  limcun  23465  dvidlem  23485  cpnord  23504  dvaddf  23511  dvmulf  23512  dvcmulf  23514  dvcof  23517  dvcj  23519  dvrec  23524  dvmptcl  23528  dvcnvlem  23543  dvcnv  23544  rolle  23557  cmvth  23558  mvth  23559  dvlip  23560  dvlipcn  23561  c1lip2  23565  dv11cn  23568  dvivthlem1  23575  dvivthlem2  23576  dvivth  23577  dvne0  23578  lhop1lem  23580  lhop1  23581  lhop2  23582  lhop  23583  dvcnvrelem2  23585  taylthlem1  23931  taylthlem2  23932  ulmf2  23942  ulm2  23943  ulmdv  23961  pserdv  23987  rlimcxp  24500  o1cxp  24501  dchrptlem2  24790  axlowdimlem5  25626  axlowdimlem7  25628  axlowdimlem10  25631  uhgrn0  25733  wrdupgr  25752  upgrfn  25754  wrdumgr  25763  umgrfn  25765  upgr1e  25779  uhgraun  25840  wrdumgra  25845  umgraf  25847  umgra1  25855  umgraun  25857  wlkelwrd  26058  2trllemH  26082  2trllemG  26088  is2wlk  26095  redwlk  26136  usgra2adedgwlkonALT  26144  usgra2wlkspthlem1  26147  usgra2wlkspthlem2  26148  fargshiftf  26164  3v3e3cycl1  26172  4cycl4v4e  26194  4cycl4dv  26195  4cycl4dv4e  26196  wlkiswwlk2lem3  26221  wlkiswwlk2  26225  vfwlkniswwlkn  26234  clwlkisclwwlklem2a  26313  clwlkisclwwlklem2  26314  clwlkfclwwlk2wrd  26367  clwlkf1clwwlklem3  26375  el2wlkonotlem  26389  eupai  26494  eupatrl  26495  eupa0  26501  eupares  26502  eupap1  26503  isgrpo  26735  vciOLD  26800  isvclem  26816  isnvlem  26849  ajfval  27048  acunirnmpt2  28842  acunirnmpt2f  28843  smatrcl  29190  locfinref  29236  1stmbfm  29649  2ndmbfm  29650  sibfof  29729  rrvf2  29837  signshf  29991  cvmliftmolem1  30517  cvmliftlem7  30527  cvmliftlem10  30530  cvmlift2lem9  30547  filnetlem4  31546  poimirlem16  32595  poimirlem19  32598  poimirlem23  32602  poimirlem24  32603  poimirlem25  32604  poimirlem29  32608  poimirlem31  32610  sdclem2  32708  sdclem1  32709  sdc  32710  fdc  32711  sstotbnd2  32743  elghomlem1OLD  32854  rngosn3  32893  amgm4d  37525  mptelpm  38352  fsneqrn  38398  cncfuni  38772  cncfiooicclem1  38779  dvsubf  38802  dvdivf  38812  dvbdfbdioolem1  38818  ioodvbdlimc1lem1  38821  ioodvbdlimc1lem2  38822  ioodvbdlimc1  38823  ioodvbdlimc2lem  38824  ioodvbdlimc2  38825  dvnprodlem3  38838  itgsubsticclem  38867  fourierdlem48  39047  fourierdlem49  39048  fourierdlem58  39057  fourierdlem59  39058  fourierdlem60  39059  fourierdlem61  39060  fourierdlem69  39068  fourierdlem75  39074  fourierdlem81  39080  fourierdlem89  39088  fourierdlem91  39090  fourierdlem97  39096  fourierdlem113  39112  meaf  39346  ismeannd  39360  psmeasure  39364  omef  39386  isomennd  39421  hoidmvlelem2  39486  hoidmvlelem3  39487  ovnhoi  39493  hspmbllem2  39517  sssmf  39625  smfpimioompt  39671  2ffzoeq  40361  upgrres1  40532  umgrres1  40533  upgr2wlk  40876  1wlkres  40879  red1wlklem  40880  1wlkdlem1  40891  uhgr1wlkspthlem2  40960  usgr2wlkneq  40962  usgr2pthlem  40969  usgr2pth  40970  crctcsh1wlkn0  41024  1wlkiswwlks2lem3  41068  1wlkiswwlks2  41072  1wlkiswwlksupgr2  41074  wlknewwlksn  41084  clwlkclwwlklem2a  41207  clwlkclwwlklem1  41208  clwlksfclwwlk2wrd  41265  clwlksfclwwlk  41269  clwlksf1clwwlklem3  41274  11wlkdlem1  41304  upgr3v3e3cycl  41347  upgr4cycl4dv4e  41352  resmgmhm  41588  elbigolo1  42149
  Copyright terms: Public domain W3C validator