Theorem ffnd 5470

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

Syntax hints:   → wi 4   Fn wfn 5309  ⟶wf 5310

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 5318

This theorem is referenced by:  offeq  6222  caofid0l  6235  caofid0r  6236  caofid1  6237  caofid2  6238  difinfsn  7255  ctssdc  7268  nnnninfeq  7283  nninfdcinf  7326  nninfwlporlemd  7327  nninfwlporlem  7328  ofnegsub  9097  seqvalcd  10670  seq3feq2  10685  seq3feq  10689  seqf1oglem2  10729  seqfeq3  10738  ser0f  10743  facnn  10936  fac0  10937  resunimafz0  11040  wrdfn  11073  swrdvalfn  11174  pfxfn  11201  pfxid  11204  cats1un  11239  seq3shft  11335  fisumss  11889  prodf1f  12040  efcvgfsum  12164  nninfctlemfo  12547  ennnfonelemfun  12974  ennnfonelemf1  12975  prdsplusgsgrpcl  13433  prdssgrpd  13434  prdsplusgcl  13465  prdsidlem  13466  prdsmndd  13467  mhmf1o  13489  resmhm2b  13508  mhmima  13510  mhmeql  13511  gsumwmhm  13517  grpinvf1o  13589  prdsinvlem  13627  ghmrn  13780  ghmpreima  13789  ghmeql  13790  ghmnsgima  13791  ghmnsgpreima  13792  ghmeqker  13794  ghmf1o  13798  gsumfzmptfidmadd  13862  rhmf1o  14117  rnrhmsubrg  14201  psrbaglesuppg  14621  mplsubgfilemcl  14648  cnrest2  14895  lmss  14905  lmtopcnp  14909  upxp  14931  uptx  14933  cnmpt11  14942  cnmpt21  14950  cnmpt22f  14954  cnmptcom  14957  hmeof1o2  14967  psmetxrge0  14991  isxmet2d  15007  blelrnps  15078  blelrn  15079  xmetresbl  15099  comet  15158  bdxmet  15160  xmettx  15169  dvidlemap  15350  dvidrelem  15351  dvidsslem  15352  dvaddxxbr  15360  dvmulxxbr  15361  dvrecap  15372  plyaddlem1  15406  upgredg  15927  nninfall  16306  nninfsellemeqinf  16313  nninffeq  16317  nnnninfex  16319  nninfnfiinf  16320  refeq  16327