Theorem ffnd 5273

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

Syntax hints:   → wi 4   Fn wfn 5118  ⟶wf 5119

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 5127

This theorem is referenced by:  offeq  5995  difinfsn  6985  ctssdc  6998  seqvalcd  10232  seq3feq2  10243  seq3feq  10245  seqfeq3  10285  ser0f  10288  facnn  10473  fac0  10474  resunimafz0  10574  seq3shft  10610  fisumss  11161  prodf1f  11312  efcvgfsum  11373  ennnfonelemfun  11930  ennnfonelemf1  11931  cnrest2  12405  lmss  12415  lmtopcnp  12419  upxp  12441  uptx  12443  cnmpt11  12452  cnmpt21  12460  cnmpt22f  12464  cnmptcom  12467  hmeof1o2  12477  psmetxrge0  12501  isxmet2d  12517  blelrnps  12588  blelrn  12589  xmetresbl  12609  comet  12668  bdxmet  12670  xmettx  12679  dvidlemap  12829  dvaddxxbr  12834  dvmulxxbr  12835  dvrecap  12846  nninfalllemn  13202  nninfall  13204  nninfsellemeqinf  13212  nninffeq  13216  refeq  13223