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  7441  ctssdc  7454  nnnninfeq  7469  nninfdcinf  7512  nninfwlporlemd  7513  nninfwlporlem  7514  ofnegsub  9295  seqvalcd  10913  seq3feq2  10928  seq3feq  10932  seqf1oglem2  10972  seqfeq3  10981  ser0f  10986  facnn  11181  fac0  11182  resunimafz0  11290  wrdfn  11335  swrdvalfn  11444  pfxfn  11471  pfxid  11474  cats1un  11509  seq3shft  11619  fisumss  12178  prodf1f  12329  efcvgfsum  12453  nninfctlemfo  12836  ennnfonelemfun  13360  ennnfonelemf1  13361  mhmf1o  13830  resmhm2b  13849  mhmima  13851  mhmeql  13852  gzsumwmhm  13856  grpinvf1o  13928  ghmrn  14113  ghmpreima  14122  ghmeql  14123  ghmnsgima  14124  ghmnsgpreima  14125  ghmeqker  14127  ghmf1o  14131  cntzmhm  14167  gsumclfi  14243  gsumf1ofi  14244  gsumsubmclfi  14247  prdsplusgsgrpcl  14274  prdssgrpd  14275  prdsplusgcl  14276  prdsidlem  14277  prdsmndd  14278  prdsinvlem  14280  rhmf1o  14559  rnrhmsubrg  14644  rrgsupp  14658  psrbagfsupp  15139  psrbaglesuppg  15141  psrbaglesupp  15142  psrbaglecl  15144  psrbagcon  15146  psrbaglefifi  15147  psrbagconf1o  15149  mplsubgfilemcl  15181  cnrest2  15428  lmss  15438  lmtopcnp  15442  upxp  15464  uptx  15466  cnmpt11  15475  cnmpt21  15483  cnmpt22f  15487  cnmptcom  15490  hmeof1o2  15500  psmetxrge0  15524  isxmet2d  15540  blelrnps  15611  blelrn  15612  xmetresbl  15632  comet  15691  bdxmet  15693  xmettx  15702  dvidlemap  15883  dvidrelem  15884  dvidsslem  15885  dvaddxxbr  15893  dvmulxxbr  15894  dvrecap  15905  plyaddlem1  15939  upgredg  16551  vtxedgfi  16696  vtxlpfi  16697  depindlem2  16914  depindlem3  16915  nninfall  17218  nninfsellemeqinf  17225  nninffeq  17229  nnnninfex  17231  nninfnfiinf  17232  refeq  17239