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  7441  ctssdc  7454  nnnninfeq  7469  nninfdcinf  7512  nninfwlporlemd  7513  nninfwlporlem  7514  ofnegsub  9295  seqvalcd  10912  seq3feq2  10927  seq3feq  10931  seqf1oglem2  10971  seqfeq3  10980  ser0f  10985  facnn  11180  fac0  11181  resunimafz0  11289  wrdfn  11334  swrdvalfn  11443  pfxfn  11470  pfxid  11473  cats1un  11508  seq3shft  11618  fisumss  12177  prodf1f  12328  efcvgfsum  12452  nninfctlemfo  12835  ennnfonelemfun  13359  ennnfonelemf1  13360  mhmf1o  13828  resmhm2b  13847  mhmima  13849  mhmeql  13850  gzsumwmhm  13854  grpinvf1o  13926  ghmrn  14111  ghmpreima  14120  ghmeql  14121  ghmnsgima  14122  ghmnsgpreima  14123  ghmeqker  14125  ghmf1o  14129  gsumclfi  14210  gsumf1ofi  14211  gsumsubmclfi  14214  prdsplusgsgrpcl  14241  prdssgrpd  14242  prdsplusgcl  14243  prdsidlem  14244  prdsmndd  14245  prdsinvlem  14247  rhmf1o  14526  rnrhmsubrg  14611  rrgsupp  14625  psrbagfsupp  15106  psrbaglesuppg  15108  psrbaglesupp  15109  psrbaglecl  15111  psrbagcon  15113  psrbaglefifi  15114  psrbagconf1o  15116  mplsubgfilemcl  15142  cnrest2  15389  lmss  15399  lmtopcnp  15403  upxp  15425  uptx  15427  cnmpt11  15436  cnmpt21  15444  cnmpt22f  15448  cnmptcom  15451  hmeof1o2  15461  psmetxrge0  15485  isxmet2d  15501  blelrnps  15572  blelrn  15573  xmetresbl  15593  comet  15652  bdxmet  15654  xmettx  15663  dvidlemap  15844  dvidrelem  15845  dvidsslem  15846  dvaddxxbr  15854  dvmulxxbr  15855  dvrecap  15866  plyaddlem1  15900  upgredg  16507  vtxedgfi  16652  vtxlpfi  16653  depindlem2  16870  depindlem3  16871  nninfall  17174  nninfsellemeqinf  17181  nninffeq  17185  nnnninfex  17187  nninfnfiinf  17188  refeq  17195