Theorem ffnd 5480

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

Syntax hints:   → wi 4   Fn wfn 5319  ⟶wf 5320

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 5328

This theorem is referenced by:  offeq  6244  caofid0l  6257  caofid0r  6258  caofid1  6259  caofid2  6260  difinfsn  7293  ctssdc  7306  nnnninfeq  7321  nninfdcinf  7364  nninfwlporlemd  7365  nninfwlporlem  7366  ofnegsub  9135  seqvalcd  10716  seq3feq2  10731  seq3feq  10735  seqf1oglem2  10775  seqfeq3  10784  ser0f  10789  facnn  10982  fac0  10983  resunimafz0  11088  wrdfn  11121  swrdvalfn  11230  pfxfn  11257  pfxid  11260  cats1un  11295  seq3shft  11392  fisumss  11946  prodf1f  12097  efcvgfsum  12221  nninfctlemfo  12604  ennnfonelemfun  13031  ennnfonelemf1  13032  prdsplusgsgrpcl  13490  prdssgrpd  13491  prdsplusgcl  13522  prdsidlem  13523  prdsmndd  13524  mhmf1o  13546  resmhm2b  13565  mhmima  13567  mhmeql  13568  gsumwmhm  13574  grpinvf1o  13646  prdsinvlem  13684  ghmrn  13837  ghmpreima  13846  ghmeql  13847  ghmnsgima  13848  ghmnsgpreima  13849  ghmeqker  13851  ghmf1o  13855  gsumfzmptfidmadd  13919  rhmf1o  14175  rnrhmsubrg  14259  psrbaglesuppg  14679  mplsubgfilemcl  14706  cnrest2  14953  lmss  14963  lmtopcnp  14967  upxp  14989  uptx  14991  cnmpt11  15000  cnmpt21  15008  cnmpt22f  15012  cnmptcom  15015  hmeof1o2  15025  psmetxrge0  15049  isxmet2d  15065  blelrnps  15136  blelrn  15137  xmetresbl  15157  comet  15216  bdxmet  15218  xmettx  15227  dvidlemap  15408  dvidrelem  15409  dvidsslem  15410  dvaddxxbr  15418  dvmulxxbr  15419  dvrecap  15430  plyaddlem1  15464  upgredg  15988  vtxedgfi  16100  vtxlpfi  16101  nninfall  16561  nninfsellemeqinf  16568  nninffeq  16572  nnnninfex  16574  nninfnfiinf  16575  refeq  16582