Theorem ffnd 5408

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

Syntax hints:   → wi 4   Fn wfn 5253  ⟶wf 5254

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 5262

This theorem is referenced by:  offeq  6149  difinfsn  7166  ctssdc  7179  nnnninfeq  7194  nninfdcinf  7237  nninfwlporlemd  7238  nninfwlporlem  7239  ofnegsub  8989  seqvalcd  10553  seq3feq2  10568  seq3feq  10572  seqf1oglem2  10612  seqfeq3  10621  ser0f  10626  facnn  10819  fac0  10820  resunimafz0  10923  wrdfn  10950  seq3shft  11003  fisumss  11557  prodf1f  11708  efcvgfsum  11832  nninfctlemfo  12207  ennnfonelemfun  12634  ennnfonelemf1  12635  mhmf1o  13102  resmhm2b  13121  mhmima  13123  mhmeql  13124  gsumwmhm  13130  grpinvf1o  13202  ghmrn  13387  ghmpreima  13396  ghmeql  13397  ghmnsgima  13398  ghmnsgpreima  13399  ghmeqker  13401  ghmf1o  13405  gsumfzmptfidmadd  13469  rhmf1o  13724  rnrhmsubrg  13808  psrbaglesuppg  14226  cnrest2  14472  lmss  14482  lmtopcnp  14486  upxp  14508  uptx  14510  cnmpt11  14519  cnmpt21  14527  cnmpt22f  14531  cnmptcom  14534  hmeof1o2  14544  psmetxrge0  14568  isxmet2d  14584  blelrnps  14655  blelrn  14656  xmetresbl  14676  comet  14735  bdxmet  14737  xmettx  14746  dvidlemap  14927  dvidrelem  14928  dvidsslem  14929  dvaddxxbr  14937  dvmulxxbr  14938  dvrecap  14949  plyaddlem1  14983  nninfall  15653  nninfsellemeqinf  15660  nninffeq  15664  refeq  15672