Theorem ffnd 5514

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

Step	Hyp	Ref	Expression
1		ffnd.1	. 2 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
2		ffn 5513	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   Fn wfn 5352  ⟶wf 5353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117  df-f 5361

This theorem is referenced by:  offeq  6289  caofid0l  6302  caofid0r  6303  caofid1  6304  caofid2  6305  fvdifsuppst  6457  suppsnopdc  6463  suppssdc  6473  suppssrst  6474  suppssrgst  6475  suppofss1dcl  6477  suppofss2dcl  6478  mapen  7112  difinfsn  7404  ctssdc  7417  nnnninfeq  7432  nninfdcinf  7475  nninfwlporlemd  7476  nninfwlporlem  7477  ofnegsub  9256  seqvalcd  10850  seq3feq2  10865  seq3feq  10869  seqf1oglem2  10909  seqfeq3  10918  ser0f  10923  facnn  11117  fac0  11118  resunimafz0  11226  wrdfn  11267  swrdvalfn  11376  pfxfn  11403  pfxid  11406  cats1un  11441  seq3shft  11551  fisumss  12107  prodf1f  12258  efcvgfsum  12382  nninfctlemfo  12765  ennnfonelemfun  13256  ennnfonelemf1  13257  mhmf1o  13729  resmhm2b  13748  mhmima  13750  mhmeql  13751  gsumwmhm  13757  grpinvf1o  13829  ghmrn  14014  ghmpreima  14023  ghmeql  14024  ghmnsgima  14025  ghmnsgpreima  14026  ghmeqker  14028  ghmf1o  14032  gsumfzmptfidmadd  14096  gfsumcl  14114  prdsplusgsgrpcl  14136  prdssgrpd  14137  prdsplusgcl  14138  prdsidlem  14139  prdsmndd  14140  prdsinvlem  14142  rhmf1o  14417  rnrhmsubrg  14502  rrgsupp  14516  psrbagfsupp  14949  psrbaglesuppg  14951  psrbaglesupp  14952  psrbaglecl  14954  psrbagcon  14956  psrbagconf1o  14958  mplsubgfilemcl  14984  cnrest2  15231  lmss  15241  lmtopcnp  15245  upxp  15267  uptx  15269  cnmpt11  15278  cnmpt21  15286  cnmpt22f  15290  cnmptcom  15293  hmeof1o2  15303  psmetxrge0  15327  isxmet2d  15343  blelrnps  15414  blelrn  15415  xmetresbl  15435  comet  15494  bdxmet  15496  xmettx  15505  dvidlemap  15686  dvidrelem  15687  dvidsslem  15688  dvaddxxbr  15696  dvmulxxbr  15697  dvrecap  15708  plyaddlem1  15742  upgredg  16269  vtxedgfi  16414  vtxlpfi  16415  depindlem2  16632  depindlem3  16633  nninfall  16927  nninfsellemeqinf  16934  nninffeq  16938  nnnninfex  16940  nninfnfiinf  16941  refeq  16948