Theorem ffnd 5534

Description: A mapping is a function with domain, deduction form. (Contributed by Glauco Siliprandi, 17-Aug-2020.)

Hypothesis

Ref	Expression
ffnd.1	|- ( ph -> F : A --> B )

Assertion

Ref	Expression
ffnd	|- ( ph -> F Fn A )

Proof of Theorem ffnd

Step	Hyp	Ref	Expression
1		ffnd.1	. 2 |- ( ph -> F : A --> B )
2		ffn 5533	. 2 |- ( F : A --> B -> F Fn A )
3	1, 2	syl 14	1 |- ( ph -> F Fn A )

This proof depends on syntax axioms:   -> wi 4   Fn wfn 5372   -->wf 5373

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 5381

This theorem is used by:  offeq  6316  caofid0l  6329  caofid0r  6330  caofid1  6331  caofid2  6332  fvdifsuppst  6484  suppsnopdc  6490  suppssdc  6500  suppssrst  6501  suppssrgst  6502  suppofss1dcl  6504  suppofss2dcl  6505  mapen  7146  difinfsn  7440  ctssdc  7453  nnnninfeq  7468  nninfdcinf  7511  nninfwlporlemd  7512  nninfwlporlem  7513  ofnegsub  9294  seqvalcd  10911  seq3feq2  10926  seq3feq  10930  seqf1oglem2  10970  seqfeq3  10979  ser0f  10984  facnn  11179  fac0  11180  resunimafz0  11288  wrdfn  11333  swrdvalfn  11442  pfxfn  11469  pfxid  11472  cats1un  11507  seq3shft  11617  fisumss  12175  prodf1f  12326  efcvgfsum  12450  nninfctlemfo  12833  ennnfonelemfun  13357  ennnfonelemf1  13358  mhmf1o  13826  resmhm2b  13845  mhmima  13847  mhmeql  13848  gzsumwmhm  13852  grpinvf1o  13924  ghmrn  14109  ghmpreima  14118  ghmeql  14119  ghmnsgima  14120  ghmnsgpreima  14121  ghmeqker  14123  ghmf1o  14127  gsumclfi  14208  gsumf1ofi  14209  gsumsubmclfi  14212  prdsplusgsgrpcl  14239  prdssgrpd  14240  prdsplusgcl  14241  prdsidlem  14242  prdsmndd  14243  prdsinvlem  14245  rhmf1o  14524  rnrhmsubrg  14609  rrgsupp  14623  psrbagfsupp  15104  psrbaglesuppg  15106  psrbaglesupp  15107  psrbaglecl  15109  psrbagcon  15111  psrbagconf1o  15113  mplsubgfilemcl  15139  cnrest2  15386  lmss  15396  lmtopcnp  15400  upxp  15422  uptx  15424  cnmpt11  15433  cnmpt21  15441  cnmpt22f  15445  cnmptcom  15448  hmeof1o2  15458  psmetxrge0  15482  isxmet2d  15498  blelrnps  15569  blelrn  15570  xmetresbl  15590  comet  15649  bdxmet  15651  xmettx  15660  dvidlemap  15841  dvidrelem  15842  dvidsslem  15843  dvaddxxbr  15851  dvmulxxbr  15852  dvrecap  15863  plyaddlem1  15897  upgredg  16483  vtxedgfi  16628  vtxlpfi  16629  depindlem2  16846  depindlem3  16847  nninfall  17150  nninfsellemeqinf  17157  nninffeq  17161  nnnninfex  17163  nninfnfiinf  17164  refeq  17171