Theorem ffnd 5483

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 5482	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   Fn wfn 5321  ⟶wf 5322

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 5330

This theorem is referenced by:  offeq  6249  caofid0l  6262  caofid0r  6263  caofid1  6264  caofid2  6265  difinfsn  7299  ctssdc  7312  nnnninfeq  7327  nninfdcinf  7370  nninfwlporlemd  7371  nninfwlporlem  7372  ofnegsub  9142  seqvalcd  10724  seq3feq2  10739  seq3feq  10743  seqf1oglem2  10783  seqfeq3  10792  ser0f  10797  facnn  10990  fac0  10991  resunimafz0  11096  wrdfn  11132  swrdvalfn  11241  pfxfn  11268  pfxid  11271  cats1un  11306  seq3shft  11403  fisumss  11958  prodf1f  12109  efcvgfsum  12233  nninfctlemfo  12616  ennnfonelemfun  13043  ennnfonelemf1  13044  prdsplusgsgrpcl  13502  prdssgrpd  13503  prdsplusgcl  13534  prdsidlem  13535  prdsmndd  13536  mhmf1o  13558  resmhm2b  13577  mhmima  13579  mhmeql  13580  gsumwmhm  13586  grpinvf1o  13658  prdsinvlem  13696  ghmrn  13849  ghmpreima  13858  ghmeql  13859  ghmnsgima  13860  ghmnsgpreima  13861  ghmeqker  13863  ghmf1o  13867  gsumfzmptfidmadd  13931  rhmf1o  14188  rnrhmsubrg  14272  psrbaglesuppg  14692  mplsubgfilemcl  14719  cnrest2  14966  lmss  14976  lmtopcnp  14980  upxp  15002  uptx  15004  cnmpt11  15013  cnmpt21  15021  cnmpt22f  15025  cnmptcom  15028  hmeof1o2  15038  psmetxrge0  15062  isxmet2d  15078  blelrnps  15149  blelrn  15150  xmetresbl  15170  comet  15229  bdxmet  15231  xmettx  15240  dvidlemap  15421  dvidrelem  15422  dvidsslem  15423  dvaddxxbr  15431  dvmulxxbr  15432  dvrecap  15443  plyaddlem1  15477  upgredg  16001  vtxedgfi  16146  vtxlpfi  16147  depindlem2  16352  depindlem3  16353  nninfall  16637  nninfsellemeqinf  16644  nninffeq  16648  nnnninfex  16650  nninfnfiinf  16651  refeq  16658  gfsumcl  16713