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  suppinisegdc  6513  mapen  7152  funisfsuppdc  7299  difinfsn  7447  ctssdc  7460  nnnninfeq  7475  nninfdcinf  7518  nninfwlporlemd  7519  nninfwlporlem  7520  ofsubeq0  9301  ofnegsub  9302  seqvalcd  10919  seq3feq2  10934  seq3feq  10938  seqf1oglem2  10978  seqfeq3  10987  ser0f  10992  facnn  11187  fac0  11188  resunimafz0  11296  wrdfn  11341  swrdvalfn  11450  pfxfn  11477  pfxid  11480  cats1un  11515  seq3shft  11625  fisumss  12184  prodf1f  12335  efcvgfsum  12459  nninfctlemfo  12842  ennnfonelemfun  13366  ennnfonelemf1  13367  mhmf1o  13836  resmhm2b  13855  mhmima  13857  mhmeql  13858  gzsumwmhm  13862  grpinvf1o  13934  ghmrn  14119  ghmpreima  14128  ghmeql  14129  ghmnsgima  14130  ghmnsgpreima  14131  ghmeqker  14133  ghmf1o  14137  cntzmhm  14173  gsumclfi  14249  gsumf1ofi  14250  gsumsubmclfi  14253  prdsplusgsgrpcl  14297  prdssgrpd  14298  prdsplusgcl  14299  prdsidlem  14300  prdsmndd  14301  prdsinvlem  14303  rhmf1o  14584  rnrhmsubrg  14669  rrgsupp  14683  psrbaglesuppg  15171  psrbaglesupp  15172  psrbaglecl  15173  psrbagcon  15174  psrbaglefifi  15175  psrbagconf1o  15177  psrbagleadd1fi  15179  ofrle2add  15180  ofpncan3  15181  psrbaglefimap  15183  psrbagmaxlem1x  15188  psrbagmaxlem1y  15189  psrbagdcle  15191  psrbagfsuppub  15192  gsumbagdiaglem  15194  psrass1filem  15196  psrlidmfi  15219  psrridmfi  15220  psrass1fi  15221  psrdifi  15222  psrdirfi  15223  mvrf2fi  15239  mplsubgfilemcl  15246  mplsubgfileminv  15247  cnrest2  15495  lmss  15505  lmtopcnp  15509  upxp  15531  uptx  15533  cnmpt11  15542  cnmpt21  15550  cnmpt22f  15554  cnmptcom  15557  hmeof1o2  15567  psmetxrge0  15591  isxmet2d  15607  blelrnps  15678  blelrn  15679  xmetresbl  15699  comet  15758  bdxmet  15760  xmettx  15769  dvidlemap  15950  dvidrelem  15951  dvidsslem  15952  dvaddxxbr  15960  dvmulxxbr  15961  dvrecap  15972  plyaddlem1  16006  upgredg  16623  vtxedgfi  16768  vtxlpfi  16769  depindlem2  16986  depindlem3  16987  nninfall  17291  nninfsellemeqinf  17298  nninffeq  17302  nnnninfex  17304  nninfnfiinf  17305  refeq  17312