Theorem ffnd 5534

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

This proof depends on syntax axioms:   → wi 4   Fn wfn 5372  ⟶wf 5373

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-f 5381

This theorem is used by:  offeq  6316  caofid0l  6329  caofid0r  6330  caofid1  6331  caofid2  6332  fvdifsuppst  6484  suppsnopdc  6490  suppssdc  6500  suppssrst  6501  suppssrgst  6502  suppofss1dcl  6504  suppofss2dcl  6505  mapen  7146  difinfsn  7440  ctssdc  7453  nnnninfeq  7468  nninfdcinf  7511  nninfwlporlemd  7512  nninfwlporlem  7513  ofnegsub  9293  seqvalcd  10900  seq3feq2  10915  seq3feq  10919  seqf1oglem2  10959  seqfeq3  10968  ser0f  10973  facnn  11167  fac0  11168  resunimafz0  11276  wrdfn  11321  swrdvalfn  11430  pfxfn  11457  pfxid  11460  cats1un  11495  seq3shft  11605  fisumss  12161  prodf1f  12312  efcvgfsum  12436  nninfctlemfo  12819  ennnfonelemfun  13310  ennnfonelemf1  13311  mhmf1o  13779  resmhm2b  13798  mhmima  13800  mhmeql  13801  gzsumwmhm  13805  grpinvf1o  13877  ghmrn  14062  ghmpreima  14071  ghmeql  14072  ghmnsgima  14073  ghmnsgpreima  14074  ghmeqker  14076  ghmf1o  14080  gsumclfi  14161  gsumf1ofi  14162  gsumsubmclfi  14165  prdsplusgsgrpcl  14192  prdssgrpd  14193  prdsplusgcl  14194  prdsidlem  14195  prdsmndd  14196  prdsinvlem  14198  rhmf1o  14477  rnrhmsubrg  14562  rrgsupp  14576  psrbagfsupp  15057  psrbaglesuppg  15059  psrbaglesupp  15060  psrbaglecl  15062  psrbagcon  15064  psrbagconf1o  15066  mplsubgfilemcl  15092  cnrest2  15339  lmss  15349  lmtopcnp  15353  upxp  15375  uptx  15377  cnmpt11  15386  cnmpt21  15394  cnmpt22f  15398  cnmptcom  15401  hmeof1o2  15411  psmetxrge0  15435  isxmet2d  15451  blelrnps  15522  blelrn  15523  xmetresbl  15543  comet  15602  bdxmet  15604  xmettx  15613  dvidlemap  15794  dvidrelem  15795  dvidsslem  15796  dvaddxxbr  15804  dvmulxxbr  15805  dvrecap  15816  plyaddlem1  15850  upgredg  16397  vtxedgfi  16542  vtxlpfi  16543  depindlem2  16760  depindlem3  16761  nninfall  17064  nninfsellemeqinf  17071  nninffeq  17075  nnnninfex  17077  nninfnfiinf  17078  refeq  17085