Theorem ffnd 5411

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

Syntax hints:   → wi 4   Fn wfn 5254  ⟶wf 5255

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 5263

This theorem is referenced by:  offeq  6153  caofid0l  6166  caofid0r  6167  caofid1  6168  caofid2  6169  difinfsn  7175  ctssdc  7188  nnnninfeq  7203  nninfdcinf  7246  nninfwlporlemd  7247  nninfwlporlem  7248  ofnegsub  9008  seqvalcd  10572  seq3feq2  10587  seq3feq  10591  seqf1oglem2  10631  seqfeq3  10640  ser0f  10645  facnn  10838  fac0  10839  resunimafz0  10942  wrdfn  10969  seq3shft  11022  fisumss  11576  prodf1f  11727  efcvgfsum  11851  nninfctlemfo  12234  ennnfonelemfun  12661  ennnfonelemf1  12662  prdsplusgsgrpcl  13118  prdssgrpd  13119  prdsplusgcl  13150  prdsidlem  13151  prdsmndd  13152  mhmf1o  13174  resmhm2b  13193  mhmima  13195  mhmeql  13196  gsumwmhm  13202  grpinvf1o  13274  prdsinvlem  13312  ghmrn  13465  ghmpreima  13474  ghmeql  13475  ghmnsgima  13476  ghmnsgpreima  13477  ghmeqker  13479  ghmf1o  13483  gsumfzmptfidmadd  13547  rhmf1o  13802  rnrhmsubrg  13886  psrbaglesuppg  14306  mplsubgfilemcl  14333  cnrest2  14580  lmss  14590  lmtopcnp  14594  upxp  14616  uptx  14618  cnmpt11  14627  cnmpt21  14635  cnmpt22f  14639  cnmptcom  14642  hmeof1o2  14652  psmetxrge0  14676  isxmet2d  14692  blelrnps  14763  blelrn  14764  xmetresbl  14784  comet  14843  bdxmet  14845  xmettx  14854  dvidlemap  15035  dvidrelem  15036  dvidsslem  15037  dvaddxxbr  15045  dvmulxxbr  15046  dvrecap  15057  plyaddlem1  15091  nninfall  15764  nninfsellemeqinf  15771  nninffeq  15775  nnnninfex  15777  nninfnfiinf  15778  refeq  15785