Theorem ffnd 5281

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

Syntax hints:   → wi 4   Fn wfn 5126  ⟶wf 5127

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

This theorem depends on definitions:  df-bi 116  df-f 5135

This theorem is referenced by:  offeq  6003  difinfsn  6993  ctssdc  7006  seqvalcd  10263  seq3feq2  10274  seq3feq  10276  seqfeq3  10316  ser0f  10319  facnn  10505  fac0  10506  resunimafz0  10606  seq3shft  10642  fisumss  11193  prodf1f  11344  efcvgfsum  11410  ennnfonelemfun  11966  ennnfonelemf1  11967  cnrest2  12444  lmss  12454  lmtopcnp  12458  upxp  12480  uptx  12482  cnmpt11  12491  cnmpt21  12499  cnmpt22f  12503  cnmptcom  12506  hmeof1o2  12516  psmetxrge0  12540  isxmet2d  12556  blelrnps  12627  blelrn  12628  xmetresbl  12648  comet  12707  bdxmet  12709  xmettx  12718  dvidlemap  12868  dvaddxxbr  12873  dvmulxxbr  12874  dvrecap  12885  nninfalllemn  13377  nninfall  13379  nninfsellemeqinf  13387  nninffeq  13391  refeq  13398