Theorem ffnd 5490

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 5489	. 2 |- ( F : A --> B -> F Fn A )
3	1, 2	syl 14	1 |- ( ph -> F Fn A )

Syntax hints:   -> wi 4   Fn wfn 5328   -->wf 5329

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 5337

This theorem is referenced by:  offeq  6258  caofid0l  6271  caofid0r  6272  caofid1  6273  caofid2  6274  fvdifsuppst  6422  suppsnopdc  6428  suppssdc  6438  suppssrst  6439  suppssrgst  6440  suppofss1dcl  6442  suppofss2dcl  6443  difinfsn  7359  ctssdc  7372  nnnninfeq  7387  nninfdcinf  7430  nninfwlporlemd  7431  nninfwlporlem  7432  ofnegsub  9201  seqvalcd  10786  seq3feq2  10801  seq3feq  10805  seqf1oglem2  10845  seqfeq3  10854  ser0f  10859  facnn  11052  fac0  11053  resunimafz0  11158  wrdfn  11194  swrdvalfn  11303  pfxfn  11330  pfxid  11333  cats1un  11368  seq3shft  11478  fisumss  12033  prodf1f  12184  efcvgfsum  12308  nninfctlemfo  12691  ennnfonelemfun  13118  ennnfonelemf1  13119  prdsplusgsgrpcl  13577  prdssgrpd  13578  prdsplusgcl  13609  prdsidlem  13610  prdsmndd  13611  mhmf1o  13633  resmhm2b  13652  mhmima  13654  mhmeql  13655  gsumwmhm  13661  grpinvf1o  13733  prdsinvlem  13771  ghmrn  13924  ghmpreima  13933  ghmeql  13934  ghmnsgima  13935  ghmnsgpreima  13936  ghmeqker  13938  ghmf1o  13942  gsumfzmptfidmadd  14006  rhmf1o  14263  rnrhmsubrg  14347  rrgsupp  14361  psrbaglesuppg  14768  psrbaglesupp  14769  psrbaglecl  14771  psrbagcon  14772  psrbagconf1o  14774  mplsubgfilemcl  14800  cnrest2  15047  lmss  15057  lmtopcnp  15061  upxp  15083  uptx  15085  cnmpt11  15094  cnmpt21  15102  cnmpt22f  15106  cnmptcom  15109  hmeof1o2  15119  psmetxrge0  15143  isxmet2d  15159  blelrnps  15230  blelrn  15231  xmetresbl  15251  comet  15310  bdxmet  15312  xmettx  15321  dvidlemap  15502  dvidrelem  15503  dvidsslem  15504  dvaddxxbr  15512  dvmulxxbr  15513  dvrecap  15524  plyaddlem1  15558  upgredg  16085  vtxedgfi  16230  vtxlpfi  16231  depindlem2  16448  depindlem3  16449  nninfall  16735  nninfsellemeqinf  16742  nninffeq  16746  nnnninfex  16748  nninfnfiinf  16749  refeq  16756  gfsumcl  16816