Theorem ffnd 5385

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

Syntax hints:   → wi 4   Fn wfn 5230  ⟶wf 5231

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 5239

This theorem is referenced by:  offeq  6121  difinfsn  7130  ctssdc  7143  nnnninfeq  7157  nninfdcinf  7200  nninfwlporlemd  7201  nninfwlporlem  7202  seqvalcd  10492  seq3feq2  10503  seq3feq  10505  seqfeq3  10545  ser0f  10549  facnn  10742  fac0  10743  resunimafz0  10846  seq3shft  10882  fisumss  11435  prodf1f  11586  efcvgfsum  11710  ennnfonelemfun  12471  ennnfonelemf1  12472  mhmf1o  12937  resmhm2b  12956  mhmima  12958  mhmeql  12959  grpinvf1o  13029  ghmrn  13213  ghmpreima  13222  ghmeql  13223  ghmnsgima  13224  ghmnsgpreima  13225  ghmeqker  13227  ghmf1o  13231  rhmf1o  13535  psrbaglesuppg  13967  cnrest2  14213  lmss  14223  lmtopcnp  14227  upxp  14249  uptx  14251  cnmpt11  14260  cnmpt21  14268  cnmpt22f  14272  cnmptcom  14275  hmeof1o2  14285  psmetxrge0  14309  isxmet2d  14325  blelrnps  14396  blelrn  14397  xmetresbl  14417  comet  14476  bdxmet  14478  xmettx  14487  dvidlemap  14637  dvaddxxbr  14642  dvmulxxbr  14643  dvrecap  14654  nninfall  15237  nninfsellemeqinf  15244  nninffeq  15248  refeq  15255