Theorem ffnd 5446

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

Syntax hints:   -> wi 4   Fn wfn 5285   -->wf 5286

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 5294

This theorem is referenced by:  offeq  6195  caofid0l  6208  caofid0r  6209  caofid1  6210  caofid2  6211  difinfsn  7228  ctssdc  7241  nnnninfeq  7256  nninfdcinf  7299  nninfwlporlemd  7300  nninfwlporlem  7301  ofnegsub  9070  seqvalcd  10643  seq3feq2  10658  seq3feq  10662  seqf1oglem2  10702  seqfeq3  10711  ser0f  10716  facnn  10909  fac0  10910  resunimafz0  11013  wrdfn  11046  swrdvalfn  11147  pfxfn  11174  pfxid  11177  cats1un  11212  seq3shft  11264  fisumss  11818  prodf1f  11969  efcvgfsum  12093  nninfctlemfo  12476  ennnfonelemfun  12903  ennnfonelemf1  12904  prdsplusgsgrpcl  13361  prdssgrpd  13362  prdsplusgcl  13393  prdsidlem  13394  prdsmndd  13395  mhmf1o  13417  resmhm2b  13436  mhmima  13438  mhmeql  13439  gsumwmhm  13445  grpinvf1o  13517  prdsinvlem  13555  ghmrn  13708  ghmpreima  13717  ghmeql  13718  ghmnsgima  13719  ghmnsgpreima  13720  ghmeqker  13722  ghmf1o  13726  gsumfzmptfidmadd  13790  rhmf1o  14045  rnrhmsubrg  14129  psrbaglesuppg  14549  mplsubgfilemcl  14576  cnrest2  14823  lmss  14833  lmtopcnp  14837  upxp  14859  uptx  14861  cnmpt11  14870  cnmpt21  14878  cnmpt22f  14882  cnmptcom  14885  hmeof1o2  14895  psmetxrge0  14919  isxmet2d  14935  blelrnps  15006  blelrn  15007  xmetresbl  15027  comet  15086  bdxmet  15088  xmettx  15097  dvidlemap  15278  dvidrelem  15279  dvidsslem  15280  dvaddxxbr  15288  dvmulxxbr  15289  dvrecap  15300  plyaddlem1  15334  upgredg  15848  nninfall  16148  nninfsellemeqinf  16155  nninffeq  16159  nnnninfex  16161  nninfnfiinf  16162  refeq  16169