Theorem ffnd 5532

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

Syntax hints:   → wi 4   Fn wfn 5370  ⟶wf 5371

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 5379

This theorem is referenced by:  offeq  6310  caofid0l  6323  caofid0r  6324  caofid1  6325  caofid2  6326  fvdifsuppst  6478  suppsnopdc  6484  suppssdc  6494  suppssrst  6495  suppssrgst  6496  suppofss1dcl  6498  suppofss2dcl  6499  mapen  7140  difinfsn  7434  ctssdc  7447  nnnninfeq  7462  nninfdcinf  7505  nninfwlporlemd  7506  nninfwlporlem  7507  ofnegsub  9286  seqvalcd  10881  seq3feq2  10896  seq3feq  10900  seqf1oglem2  10940  seqfeq3  10949  ser0f  10954  facnn  11148  fac0  11149  resunimafz0  11257  wrdfn  11302  swrdvalfn  11411  pfxfn  11438  pfxid  11441  cats1un  11476  seq3shft  11586  fisumss  12142  prodf1f  12293  efcvgfsum  12417  nninfctlemfo  12800  ennnfonelemfun  13291  ennnfonelemf1  13292  mhmf1o  13760  resmhm2b  13779  mhmima  13781  mhmeql  13782  gzsumwmhm  13786  grpinvf1o  13858  ghmrn  14043  ghmpreima  14052  ghmeql  14053  ghmnsgima  14054  ghmnsgpreima  14055  ghmeqker  14057  ghmf1o  14061  gsumclfi  14142  gsumf1ofi  14143  gsumsubmclfi  14146  prdsplusgsgrpcl  14173  prdssgrpd  14174  prdsplusgcl  14175  prdsidlem  14176  prdsmndd  14177  prdsinvlem  14179  rhmf1o  14458  rnrhmsubrg  14543  rrgsupp  14557  psrbagfsupp  15038  psrbaglesuppg  15040  psrbaglesupp  15041  psrbaglecl  15043  psrbagcon  15045  psrbagconf1o  15047  mplsubgfilemcl  15073  cnrest2  15320  lmss  15330  lmtopcnp  15334  upxp  15356  uptx  15358  cnmpt11  15367  cnmpt21  15375  cnmpt22f  15379  cnmptcom  15382  hmeof1o2  15392  psmetxrge0  15416  isxmet2d  15432  blelrnps  15503  blelrn  15504  xmetresbl  15524  comet  15583  bdxmet  15585  xmettx  15594  dvidlemap  15775  dvidrelem  15776  dvidsslem  15777  dvaddxxbr  15785  dvmulxxbr  15786  dvrecap  15797  plyaddlem1  15831  upgredg  16368  vtxedgfi  16513  vtxlpfi  16514  depindlem2  16731  depindlem3  16732  nninfall  17026  nninfsellemeqinf  17033  nninffeq  17037  nnnninfex  17039  nninfnfiinf  17040  refeq  17047