Theorem ffnd 5508

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

Syntax hints:   → wi 4   Fn wfn 5346  ⟶wf 5347

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 5355

This theorem is referenced by:  offeq  6279  caofid0l  6292  caofid0r  6293  caofid1  6294  caofid2  6295  fvdifsuppst  6443  suppsnopdc  6449  suppssdc  6459  suppssrst  6460  suppssrgst  6461  suppofss1dcl  6463  suppofss2dcl  6464  mapen  7098  difinfsn  7390  ctssdc  7403  nnnninfeq  7418  nninfdcinf  7461  nninfwlporlemd  7462  nninfwlporlem  7463  ofnegsub  9235  seqvalcd  10822  seq3feq2  10837  seq3feq  10841  seqf1oglem2  10881  seqfeq3  10890  ser0f  10895  facnn  11088  fac0  11089  resunimafz0  11194  wrdfn  11235  swrdvalfn  11344  pfxfn  11371  pfxid  11374  cats1un  11409  seq3shft  11519  fisumss  12074  prodf1f  12225  efcvgfsum  12349  nninfctlemfo  12732  ennnfonelemfun  13160  ennnfonelemf1  13161  prdsplusgsgrpcl  13619  prdssgrpd  13620  prdsplusgcl  13651  prdsidlem  13652  prdsmndd  13653  mhmf1o  13675  resmhm2b  13694  mhmima  13696  mhmeql  13697  gsumwmhm  13703  grpinvf1o  13775  prdsinvlem  13813  ghmrn  13966  ghmpreima  13975  ghmeql  13976  ghmnsgima  13977  ghmnsgpreima  13978  ghmeqker  13980  ghmf1o  13984  gsumfzmptfidmadd  14048  rhmf1o  14305  rnrhmsubrg  14389  rrgsupp  14403  psrbagfsupp  14811  psrbaglesuppg  14813  psrbaglesupp  14814  psrbaglecl  14816  psrbagcon  14818  psrbagconf1o  14820  mplsubgfilemcl  14846  cnrest2  15093  lmss  15103  lmtopcnp  15107  upxp  15129  uptx  15131  cnmpt11  15140  cnmpt21  15148  cnmpt22f  15152  cnmptcom  15155  hmeof1o2  15165  psmetxrge0  15189  isxmet2d  15205  blelrnps  15276  blelrn  15277  xmetresbl  15297  comet  15356  bdxmet  15358  xmettx  15367  dvidlemap  15548  dvidrelem  15549  dvidsslem  15550  dvaddxxbr  15558  dvmulxxbr  15559  dvrecap  15570  plyaddlem1  15604  upgredg  16131  vtxedgfi  16276  vtxlpfi  16277  depindlem2  16494  depindlem3  16495  nninfall  16779  nninfsellemeqinf  16786  nninffeq  16790  nnnninfex  16792  nninfnfiinf  16793  refeq  16800  gfsumcl  16861