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

Theorem ffnd 6199
Description: A mapping is a function with domain, deduction form. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypothesis
Ref Expression
ffnd.1 (𝜑𝐹:𝐴𝐵)
Assertion
Ref Expression
ffnd (𝜑𝐹 Fn 𝐴)

Proof of Theorem ffnd
StepHypRef Expression
1 ffnd.1 . 2 (𝜑𝐹:𝐴𝐵)
2 ffn 6198 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
31, 2syl 17 1 (𝜑𝐹 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Fn wfn 6036  wf 6037
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-an 385  df-f 6045
This theorem is referenced by:  fofn  6270  oprres  6959  fnwelem  7452  resunimafz0  13413  cats1un  13667  isacs4lem  17361  gsumzaddlem  18513  ablfac1eu  18664  lmodfopnelem1  19093  psrbaglefi  19566  psrvscaval  19586  psrlidm  19597  psrridm  19598  psrass1  19599  psrdi  19600  psrdir  19601  mplsubglem  19628  mplvscaval  19642  mplbas2  19664  evlslem3  19708  evlslem1  19709  evlsvar  19717  ptbasfi  21578  rrxmet  23383  itg2cnlem2  23720  mdegldg  24017  fta1glem2  24117  fta1blem  24119  aannenlem1  24274  dchrisum0re  25393  vtxdgfisf  26574  2pthon3v  27055  ofpreima2  29767  reprsuc  30994  circlemethhgt  31022  hgt750lemb  31035  matunitlindflem1  33710  mblfinlem2  33752  fsovf1od  38804  brcoffn  38822  clsneiel1  38900  ssmapsn  39899  preimaiocmnf  40283  fsumsupp0  40305  climinf2lem  40433  limsupmnflem  40447  limsupvaluz2  40465  supcnvlimsup  40467  limsupgtlem  40504  liminfvalxr  40510  liminflelimsupuz  40512  xlimconst2  40556  climxlim2  40567  volicoff  40707  sge0resrn  41116  sge0le  41119  sge0fodjrnlem  41128  sge0seq  41158  nnfoctbdjlem  41167  meadjiunlem  41177  omeiunle  41229  hoicvr  41260  ovnovollem1  41368  ovnovollem2  41369  iinhoiicclem  41385  iunhoiioolem  41387  preimaicomnf  41420  smfresal  41493  smfsuplem1  41515  smflimsuplem2  41525  amgmwlem  43053
  Copyright terms: Public domain W3C validator