Theorem ffnd 5490

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 5489	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   Fn wfn 5328  ⟶wf 5329

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 5337

This theorem is referenced by:  offeq  6258  caofid0l  6271  caofid0r  6272  caofid1  6273  caofid2  6274  fvdifsuppst  6422  suppsnopdc  6428  suppssdc  6438  suppssrst  6439  suppssrgst  6440  suppofss1dcl  6442  suppofss2dcl  6443  difinfsn  7342  ctssdc  7355  nnnninfeq  7370  nninfdcinf  7413  nninfwlporlemd  7414  nninfwlporlem  7415  ofnegsub  9185  seqvalcd  10767  seq3feq2  10782  seq3feq  10786  seqf1oglem2  10826  seqfeq3  10835  ser0f  10840  facnn  11033  fac0  11034  resunimafz0  11139  wrdfn  11175  swrdvalfn  11284  pfxfn  11311  pfxid  11314  cats1un  11349  seq3shft  11459  fisumss  12014  prodf1f  12165  efcvgfsum  12289  nninfctlemfo  12672  ennnfonelemfun  13099  ennnfonelemf1  13100  prdsplusgsgrpcl  13558  prdssgrpd  13559  prdsplusgcl  13590  prdsidlem  13591  prdsmndd  13592  mhmf1o  13614  resmhm2b  13633  mhmima  13635  mhmeql  13636  gsumwmhm  13642  grpinvf1o  13714  prdsinvlem  13752  ghmrn  13905  ghmpreima  13914  ghmeql  13915  ghmnsgima  13916  ghmnsgpreima  13917  ghmeqker  13919  ghmf1o  13923  gsumfzmptfidmadd  13987  rhmf1o  14244  rnrhmsubrg  14328  psrbaglesuppg  14748  psrbaglesupp  14749  psrbaglecl  14751  psrbagcon  14752  psrbagconf1o  14754  mplsubgfilemcl  14780  cnrest2  15027  lmss  15037  lmtopcnp  15041  upxp  15063  uptx  15065  cnmpt11  15074  cnmpt21  15082  cnmpt22f  15086  cnmptcom  15089  hmeof1o2  15099  psmetxrge0  15123  isxmet2d  15139  blelrnps  15210  blelrn  15211  xmetresbl  15231  comet  15290  bdxmet  15292  xmettx  15301  dvidlemap  15482  dvidrelem  15483  dvidsslem  15484  dvaddxxbr  15492  dvmulxxbr  15493  dvrecap  15504  plyaddlem1  15538  upgredg  16065  vtxedgfi  16210  vtxlpfi  16211  depindlem2  16428  depindlem3  16429  nninfall  16715  nninfsellemeqinf  16722  nninffeq  16726  nnnninfex  16728  nninfnfiinf  16729  refeq  16736  gfsumcl  16796