Theorem ffnd 5404

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

Syntax hints:   → wi 4   Fn wfn 5249  ⟶wf 5250

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 5258

This theorem is referenced by:  offeq  6144  difinfsn  7159  ctssdc  7172  nnnninfeq  7187  nninfdcinf  7230  nninfwlporlemd  7231  nninfwlporlem  7232  ofnegsub  8981  seqvalcd  10532  seq3feq2  10547  seq3feq  10551  seqf1oglem2  10591  seqfeq3  10600  ser0f  10605  facnn  10798  fac0  10799  resunimafz0  10902  wrdfn  10929  seq3shft  10982  fisumss  11535  prodf1f  11686  efcvgfsum  11810  nninfctlemfo  12177  ennnfonelemfun  12574  ennnfonelemf1  12575  mhmf1o  13042  resmhm2b  13061  mhmima  13063  mhmeql  13064  gsumwmhm  13070  grpinvf1o  13142  ghmrn  13327  ghmpreima  13336  ghmeql  13337  ghmnsgima  13338  ghmnsgpreima  13339  ghmeqker  13341  ghmf1o  13345  gsumfzmptfidmadd  13409  rhmf1o  13664  rnrhmsubrg  13748  psrbaglesuppg  14158  cnrest2  14404  lmss  14414  lmtopcnp  14418  upxp  14440  uptx  14442  cnmpt11  14451  cnmpt21  14459  cnmpt22f  14463  cnmptcom  14466  hmeof1o2  14476  psmetxrge0  14500  isxmet2d  14516  blelrnps  14587  blelrn  14588  xmetresbl  14608  comet  14667  bdxmet  14669  xmettx  14678  dvidlemap  14845  dvaddxxbr  14850  dvmulxxbr  14851  dvrecap  14862  plyaddlem1  14893  nninfall  15499  nninfsellemeqinf  15506  nninffeq  15510  refeq  15518