Theorem ffnd 5367

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

Syntax hints:   → wi 4   Fn wfn 5212  ⟶wf 5213

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 5221

This theorem is referenced by:  offeq  6096  difinfsn  7099  ctssdc  7112  nnnninfeq  7126  nninfdcinf  7169  nninfwlporlemd  7170  nninfwlporlem  7171  seqvalcd  10459  seq3feq2  10470  seq3feq  10472  seqfeq3  10512  ser0f  10515  facnn  10707  fac0  10708  resunimafz0  10811  seq3shft  10847  fisumss  11400  prodf1f  11551  efcvgfsum  11675  ennnfonelemfun  12418  ennnfonelemf1  12419  mhmf1o  12861  mhmima  12875  mhmeql  12876  grpinvf1o  12940  cnrest2  13739  lmss  13749  lmtopcnp  13753  upxp  13775  uptx  13777  cnmpt11  13786  cnmpt21  13794  cnmpt22f  13798  cnmptcom  13801  hmeof1o2  13811  psmetxrge0  13835  isxmet2d  13851  blelrnps  13922  blelrn  13923  xmetresbl  13943  comet  14002  bdxmet  14004  xmettx  14013  dvidlemap  14163  dvaddxxbr  14168  dvmulxxbr  14169  dvrecap  14180  nninfall  14761  nninfsellemeqinf  14768  nninffeq  14772  refeq  14779