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

Theorem feq2d 6069
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 6065 . 2 (𝐴 = 𝐵 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1523  wf 5922
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-fn 5929  df-f 5930
This theorem is referenced by:  feq12d  6071  ffdm  6100  fsng  6444  fsn2g  6445  fsnunf2  6493  issmo2  7491  qliftf  7878  elpm2r  7917  ralxpmap  7949  ordtypelem5  8468  axdc3lem3  9312  axdc3lem4  9313  fseq1p1m1  12452  fseq1m1p1  12453  seqf1o  12882  iswrdi  13341  wrdf  13342  wrdffz  13358  ffz0iswrd  13364  wrdnval  13367  ccatalpha  13411  swrdf  13471  swrd0f  13473  cats1un  13521  cshwf  13592  wrdlen2i  13732  wwlktovf  13745  rlimi  14288  rlimmptrcl  14382  lo1mptrcl  14396  o1mptrcl  14397  o1fsum  14589  ram0  15773  funcres  16603  curf2cl  16918  uncfcurf  16926  yonedalem4c  16964  intopsn  17300  gsumprval  17328  resmhm  17406  gsumwsubmcl  17422  gsumccat  17425  gsumwmhm  17429  frmdup1  17448  frmdup3lem  17450  isghm  17707  resghm  17723  subgga  17779  gasubg  17781  psgnunilem2  17961  sylow2blem2  18082  pj2f  18157  pj1ghm  18162  frgpupf  18232  frgpup3lem  18236  gsumval3  18354  gsummptfzcl  18414  dprdf2  18452  ablfaclem2  18531  ablfac2  18534  isabvd  18868  abvpropd  18890  mplasclf  19545  evlssca  19570  lply1binomsc  19725  cygznlem2a  19964  frgpcyg  19970  mat1dimelbas  20325  mat2pmatbas  20579  cpmadugsumlemF  20729  cnpf2  21102  lmcnp  21156  ptpjcn  21462  cnextfres1  21919  cnextfres  21920  cnmpt2pc  22774  pi1addf  22893  pi1xfrf  22899  pi1cof  22905  mbfmptcl  23449  iblcnlem  23600  limcres  23695  cnplimc  23696  limccnp  23700  limccnp2  23701  limcun  23704  dvidlem  23724  cpnord  23743  dvaddf  23750  dvmulf  23751  dvcmulf  23753  dvcof  23756  dvcj  23758  dvrec  23763  dvmptcl  23767  dvcnvlem  23784  dvcnv  23785  rolle  23798  cmvth  23799  mvth  23800  dvlip  23801  dvlipcn  23802  c1lip2  23806  dv11cn  23809  dvivthlem1  23816  dvivthlem2  23817  dvivth  23818  dvne0  23819  lhop1lem  23821  lhop1  23822  lhop2  23823  lhop  23824  dvcnvrelem2  23826  taylthlem1  24172  taylthlem2  24173  ulmf2  24183  ulm2  24184  ulmdv  24202  pserdv  24228  rlimcxp  24745  o1cxp  24746  dchrptlem2  25035  axlowdimlem5  25871  axlowdimlem7  25873  axlowdimlem10  25876  uhgrn0  26007  wrdupgr  26025  upgrfn  26027  wrdumgr  26037  umgrfn  26039  upgr1e  26053  umgrres1  26251  upgr2wlk  26620  wlkres  26623  redwlklem  26624  wlkdlem1  26635  uhgrwkspthlem2  26706  usgr2wlkneq  26708  usgr2pthlem  26715  usgr2pth  26716  crctcshwlkn0  26769  wlkiswwlks2lem3  26825  wlkiswwlks2  26829  wlkiswwlksupgr2  26831  wlknewwlksn  26841  wpthswwlks2on  26927  clwlkclwwlklem2a  26964  clwlkclwwlklem1  26965  clwlksfclwwlk2wrd  27045  clwlksfclwwlk  27049  clwlksf1clwwlklem3  27054  1wlkdlem1  27115  upgr3v3e3cycl  27158  upgr4cycl4dv4e  27163  isgrpo  27479  vciOLD  27544  isvclem  27560  isnvlem  27593  ajfval  27792  acunirnmpt2  29588  acunirnmpt2f  29589  smatrcl  29990  locfinref  30036  1stmbfm  30450  2ndmbfm  30451  sibfof  30530  rrvf2  30638  signshf  30793  reprsuc  30821  cvmliftmolem1  31389  cvmliftlem7  31399  cvmliftlem10  31402  cvmlift2lem9  31419  filnetlem4  32501  poimirlem16  33555  poimirlem19  33558  poimirlem23  33562  poimirlem24  33563  poimirlem25  33564  poimirlem29  33568  poimirlem31  33570  sdclem2  33668  sdclem1  33669  sdc  33670  fdc  33671  sstotbnd2  33703  elghomlem1OLD  33814  rngosn3  33853  amgm4d  38820  mptelpm  39671  fsneqrn  39717  cncfuni  40417  cncfiooicclem1  40424  dvsubf  40446  dvdivf  40455  dvbdfbdioolem1  40461  ioodvbdlimc1lem1  40464  ioodvbdlimc1lem2  40465  ioodvbdlimc1  40466  ioodvbdlimc2lem  40467  ioodvbdlimc2  40468  dvnprodlem3  40481  itgsubsticclem  40509  fourierdlem48  40689  fourierdlem49  40690  fourierdlem58  40699  fourierdlem59  40700  fourierdlem60  40701  fourierdlem61  40702  fourierdlem69  40710  fourierdlem75  40716  fourierdlem81  40722  fourierdlem89  40730  fourierdlem91  40732  fourierdlem97  40738  fourierdlem113  40754  meaf  40988  ismeannd  41002  psmeasure  41006  omef  41031  isomennd  41066  hoidmvlelem2  41131  hoidmvlelem3  41132  ovnhoi  41138  hspmbllem2  41162  sssmf  41268  smfpimioompt  41314  smffmpt  41332  2ffzoeq  41663  fargshiftf  41701  resmgmhm  42123  elbigolo1  42676
  Copyright terms: Public domain W3C validator