Theorem ffnd 5348

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

Syntax hints:   → wi 4   Fn wfn 5193  ⟶wf 5194

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 5202

This theorem is referenced by:  offeq  6074  difinfsn  7077  ctssdc  7090  nnnninfeq  7104  nninfdcinf  7147  nninfwlporlemd  7148  nninfwlporlem  7149  seqvalcd  10415  seq3feq2  10426  seq3feq  10428  seqfeq3  10468  ser0f  10471  facnn  10661  fac0  10662  resunimafz0  10766  seq3shft  10802  fisumss  11355  prodf1f  11506  efcvgfsum  11630  ennnfonelemfun  12372  ennnfonelemf1  12373  mhmf1o  12693  mhmima  12706  mhmeql  12707  grpinvf1o  12769  cnrest2  13030  lmss  13040  lmtopcnp  13044  upxp  13066  uptx  13068  cnmpt11  13077  cnmpt21  13085  cnmpt22f  13089  cnmptcom  13092  hmeof1o2  13102  psmetxrge0  13126  isxmet2d  13142  blelrnps  13213  blelrn  13214  xmetresbl  13234  comet  13293  bdxmet  13295  xmettx  13304  dvidlemap  13454  dvaddxxbr  13459  dvmulxxbr  13460  dvrecap  13471  nninfall  14042  nninfsellemeqinf  14049  nninffeq  14053  refeq  14060