Theorem ffnd 5537

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

This proof depends on syntax axioms:   → wi 4   Fn wfn 5375  ⟶wf 5376

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-f 5384

This theorem is used by:  offeq  6320  caofid0l  6333  caofid0r  6334  caofid1  6335  caofid2  6336  fvdifsuppst  6488  suppsnopdc  6494  suppssdc  6504  suppssrst  6505  suppssrgst  6506  suppofss1dcl  6508  suppofss2dcl  6509  mapen  7151  difinfsn  7447  ctssdc  7460  nnnninfeq  7475  nninfdcinf  7518  nninfwlporlemd  7519  nninfwlporlem  7520  ofsubeq0  9301  ofnegsub  9302  seqvalcd  10920  seq3feq2  10935  seq3feq  10939  seqf1oglem2  10979  seqfeq3  10988  ser0f  10993  facnn  11188  fac0  11189  resunimafz0  11297  wrdfn  11342  swrdvalfn  11451  pfxfn  11478  pfxid  11481  cats1un  11516  seq3shft  11626  fisumss  12185  prodf1f  12336  efcvgfsum  12460  nninfctlemfo  12843  ennnfonelemfun  13367  ennnfonelemf1  13368  mhmf1o  13837  resmhm2b  13856  mhmima  13858  mhmeql  13859  gzsumwmhm  13863  grpinvf1o  13935  ghmrn  14120  ghmpreima  14129  ghmeql  14130  ghmnsgima  14131  ghmnsgpreima  14132  ghmeqker  14134  ghmf1o  14138  cntzmhm  14174  gsumclfi  14250  gsumf1ofi  14251  gsumsubmclfi  14254  prdsplusgsgrpcl  14298  prdssgrpd  14299  prdsplusgcl  14300  prdsidlem  14301  prdsmndd  14302  prdsinvlem  14304  rhmf1o  14585  rnrhmsubrg  14670  rrgsupp  14684  psrbagfsupp  15167  psrbaglesuppg  15172  psrbaglesupp  15173  psrbaglecl  15174  psrbagcon  15176  psrbaglefifi  15177  psrbagconf1o  15179  gsumbagdiaglem  15180  psrass1filem  15182  psrlidmfi  15204  psrridmfi  15205  psrass1fi  15206  psrdifi  15207  psrdirfi  15208  mplsubgfilemcl  15227  cnrest2  15474  lmss  15484  lmtopcnp  15488  upxp  15510  uptx  15512  cnmpt11  15521  cnmpt21  15529  cnmpt22f  15533  cnmptcom  15536  hmeof1o2  15546  psmetxrge0  15570  isxmet2d  15586  blelrnps  15657  blelrn  15658  xmetresbl  15678  comet  15737  bdxmet  15739  xmettx  15748  dvidlemap  15929  dvidrelem  15930  dvidsslem  15931  dvaddxxbr  15939  dvmulxxbr  15940  dvrecap  15951  plyaddlem1  15985  upgredg  16602  vtxedgfi  16747  vtxlpfi  16748  depindlem2  16965  depindlem3  16966  nninfall  17270  nninfsellemeqinf  17277  nninffeq  17281  nnnninfex  17283  nninfnfiinf  17284  refeq  17291