Theorem ffnd 5433

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

Syntax hints:   → wi 4   Fn wfn 5272  ⟶wf 5273

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 5281

This theorem is referenced by:  offeq  6182  caofid0l  6195  caofid0r  6196  caofid1  6197  caofid2  6198  difinfsn  7214  ctssdc  7227  nnnninfeq  7242  nninfdcinf  7285  nninfwlporlemd  7286  nninfwlporlem  7287  ofnegsub  9048  seqvalcd  10619  seq3feq2  10634  seq3feq  10638  seqf1oglem2  10678  seqfeq3  10687  ser0f  10692  facnn  10885  fac0  10886  resunimafz0  10989  wrdfn  11022  swrdvalfn  11123  pfxfn  11148  pfxid  11151  seq3shft  11199  fisumss  11753  prodf1f  11904  efcvgfsum  12028  nninfctlemfo  12411  ennnfonelemfun  12838  ennnfonelemf1  12839  prdsplusgsgrpcl  13296  prdssgrpd  13297  prdsplusgcl  13328  prdsidlem  13329  prdsmndd  13330  mhmf1o  13352  resmhm2b  13371  mhmima  13373  mhmeql  13374  gsumwmhm  13380  grpinvf1o  13452  prdsinvlem  13490  ghmrn  13643  ghmpreima  13652  ghmeql  13653  ghmnsgima  13654  ghmnsgpreima  13655  ghmeqker  13657  ghmf1o  13661  gsumfzmptfidmadd  13725  rhmf1o  13980  rnrhmsubrg  14064  psrbaglesuppg  14484  mplsubgfilemcl  14511  cnrest2  14758  lmss  14768  lmtopcnp  14772  upxp  14794  uptx  14796  cnmpt11  14805  cnmpt21  14813  cnmpt22f  14817  cnmptcom  14820  hmeof1o2  14830  psmetxrge0  14854  isxmet2d  14870  blelrnps  14941  blelrn  14942  xmetresbl  14962  comet  15021  bdxmet  15023  xmettx  15032  dvidlemap  15213  dvidrelem  15214  dvidsslem  15215  dvaddxxbr  15223  dvmulxxbr  15224  dvrecap  15235  plyaddlem1  15269  nninfall  16061  nninfsellemeqinf  16068  nninffeq  16072  nnnninfex  16074  nninfnfiinf  16075  refeq  16082