Theorem ffnd 5514

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

Syntax hints:   → wi 4   Fn wfn 5352  ⟶wf 5353

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 5361

This theorem is referenced by:  offeq  6289  caofid0l  6302  caofid0r  6303  caofid1  6304  caofid2  6305  fvdifsuppst  6457  suppsnopdc  6463  suppssdc  6473  suppssrst  6474  suppssrgst  6475  suppofss1dcl  6477  suppofss2dcl  6478  mapen  7112  difinfsn  7404  ctssdc  7417  nnnninfeq  7432  nninfdcinf  7475  nninfwlporlemd  7476  nninfwlporlem  7477  ofnegsub  9253  seqvalcd  10847  seq3feq2  10862  seq3feq  10866  seqf1oglem2  10906  seqfeq3  10915  ser0f  10920  facnn  11114  fac0  11115  resunimafz0  11223  wrdfn  11264  swrdvalfn  11373  pfxfn  11400  pfxid  11403  cats1un  11438  seq3shft  11548  fisumss  12103  prodf1f  12254  efcvgfsum  12378  nninfctlemfo  12761  ennnfonelemfun  13252  ennnfonelemf1  13253  prdsplusgsgrpcl  13711  prdssgrpd  13712  prdsplusgcl  13743  prdsidlem  13744  prdsmndd  13745  mhmf1o  13767  resmhm2b  13786  mhmima  13788  mhmeql  13789  gsumwmhm  13795  grpinvf1o  13867  prdsinvlem  13905  ghmrn  14058  ghmpreima  14067  ghmeql  14068  ghmnsgima  14069  ghmnsgpreima  14070  ghmeqker  14072  ghmf1o  14076  gsumfzmptfidmadd  14140  rhmf1o  14398  rnrhmsubrg  14483  rrgsupp  14497  psrbagfsupp  14931  psrbaglesuppg  14933  psrbaglesupp  14934  psrbaglecl  14936  psrbagcon  14938  psrbagconf1o  14940  mplsubgfilemcl  14966  cnrest2  15213  lmss  15223  lmtopcnp  15227  upxp  15249  uptx  15251  cnmpt11  15260  cnmpt21  15268  cnmpt22f  15272  cnmptcom  15275  hmeof1o2  15285  psmetxrge0  15309  isxmet2d  15325  blelrnps  15396  blelrn  15397  xmetresbl  15417  comet  15476  bdxmet  15478  xmettx  15487  dvidlemap  15668  dvidrelem  15669  dvidsslem  15670  dvaddxxbr  15678  dvmulxxbr  15679  dvrecap  15690  plyaddlem1  15724  upgredg  16251  vtxedgfi  16396  vtxlpfi  16397  depindlem2  16614  depindlem3  16615  nninfall  16899  nninfsellemeqinf  16906  nninffeq  16910  nnnninfex  16912  nninfnfiinf  16913  refeq  16920  gfsumcl  16982