Theorem ffnd 5474

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

Syntax hints:   → wi 4   Fn wfn 5313  ⟶wf 5314

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 5322

This theorem is referenced by:  offeq  6238  caofid0l  6251  caofid0r  6252  caofid1  6253  caofid2  6254  difinfsn  7275  ctssdc  7288  nnnninfeq  7303  nninfdcinf  7346  nninfwlporlemd  7347  nninfwlporlem  7348  ofnegsub  9117  seqvalcd  10691  seq3feq2  10706  seq3feq  10710  seqf1oglem2  10750  seqfeq3  10759  ser0f  10764  facnn  10957  fac0  10958  resunimafz0  11061  wrdfn  11094  swrdvalfn  11196  pfxfn  11223  pfxid  11226  cats1un  11261  seq3shft  11357  fisumss  11911  prodf1f  12062  efcvgfsum  12186  nninfctlemfo  12569  ennnfonelemfun  12996  ennnfonelemf1  12997  prdsplusgsgrpcl  13455  prdssgrpd  13456  prdsplusgcl  13487  prdsidlem  13488  prdsmndd  13489  mhmf1o  13511  resmhm2b  13530  mhmima  13532  mhmeql  13533  gsumwmhm  13539  grpinvf1o  13611  prdsinvlem  13649  ghmrn  13802  ghmpreima  13811  ghmeql  13812  ghmnsgima  13813  ghmnsgpreima  13814  ghmeqker  13816  ghmf1o  13820  gsumfzmptfidmadd  13884  rhmf1o  14140  rnrhmsubrg  14224  psrbaglesuppg  14644  mplsubgfilemcl  14671  cnrest2  14918  lmss  14928  lmtopcnp  14932  upxp  14954  uptx  14956  cnmpt11  14965  cnmpt21  14973  cnmpt22f  14977  cnmptcom  14980  hmeof1o2  14990  psmetxrge0  15014  isxmet2d  15030  blelrnps  15101  blelrn  15102  xmetresbl  15122  comet  15181  bdxmet  15183  xmettx  15192  dvidlemap  15373  dvidrelem  15374  dvidsslem  15375  dvaddxxbr  15383  dvmulxxbr  15384  dvrecap  15395  plyaddlem1  15429  upgredg  15950  nninfall  16405  nninfsellemeqinf  16412  nninffeq  16416  nnnninfex  16418  nninfnfiinf  16419  refeq  16426