Theorem ffnd 5405

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

Syntax hints:   → wi 4   Fn wfn 5250  ⟶wf 5251

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 5259

This theorem is referenced by:  offeq  6146  difinfsn  7161  ctssdc  7174  nnnninfeq  7189  nninfdcinf  7232  nninfwlporlemd  7233  nninfwlporlem  7234  ofnegsub  8983  seqvalcd  10535  seq3feq2  10550  seq3feq  10554  seqf1oglem2  10594  seqfeq3  10603  ser0f  10608  facnn  10801  fac0  10802  resunimafz0  10905  wrdfn  10932  seq3shft  10985  fisumss  11538  prodf1f  11689  efcvgfsum  11813  nninfctlemfo  12180  ennnfonelemfun  12577  ennnfonelemf1  12578  mhmf1o  13045  resmhm2b  13064  mhmima  13066  mhmeql  13067  gsumwmhm  13073  grpinvf1o  13145  ghmrn  13330  ghmpreima  13339  ghmeql  13340  ghmnsgima  13341  ghmnsgpreima  13342  ghmeqker  13344  ghmf1o  13348  gsumfzmptfidmadd  13412  rhmf1o  13667  rnrhmsubrg  13751  psrbaglesuppg  14169  cnrest2  14415  lmss  14425  lmtopcnp  14429  upxp  14451  uptx  14453  cnmpt11  14462  cnmpt21  14470  cnmpt22f  14474  cnmptcom  14477  hmeof1o2  14487  psmetxrge0  14511  isxmet2d  14527  blelrnps  14598  blelrn  14599  xmetresbl  14619  comet  14678  bdxmet  14680  xmettx  14689  dvidlemap  14870  dvidrelem  14871  dvidsslem  14872  dvaddxxbr  14880  dvmulxxbr  14881  dvrecap  14892  plyaddlem1  14926  nninfall  15569  nninfsellemeqinf  15576  nninffeq  15580  refeq  15588