Theorem ffnd 5366

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

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

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 5220

This theorem is referenced by:  offeq  6095  difinfsn  7098  ctssdc  7111  nnnninfeq  7125  nninfdcinf  7168  nninfwlporlemd  7169  nninfwlporlem  7170  seqvalcd  10458  seq3feq2  10469  seq3feq  10471  seqfeq3  10511  ser0f  10514  facnn  10706  fac0  10707  resunimafz0  10810  seq3shft  10846  fisumss  11399  prodf1f  11550  efcvgfsum  11674  ennnfonelemfun  12417  ennnfonelemf1  12418  mhmf1o  12860  mhmima  12874  mhmeql  12875  grpinvf1o  12939  cnrest2  13706  lmss  13716  lmtopcnp  13720  upxp  13742  uptx  13744  cnmpt11  13753  cnmpt21  13761  cnmpt22f  13765  cnmptcom  13768  hmeof1o2  13778  psmetxrge0  13802  isxmet2d  13818  blelrnps  13889  blelrn  13890  xmetresbl  13910  comet  13969  bdxmet  13971  xmettx  13980  dvidlemap  14130  dvaddxxbr  14135  dvmulxxbr  14136  dvrecap  14147  nninfall  14728  nninfsellemeqinf  14735  nninffeq  14739  refeq  14746