Theorem ffnd 5477

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

Syntax hints:   → wi 4   Fn wfn 5316  ⟶wf 5317

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 5325

This theorem is referenced by:  offeq  6241  caofid0l  6254  caofid0r  6255  caofid1  6256  caofid2  6257  difinfsn  7283  ctssdc  7296  nnnninfeq  7311  nninfdcinf  7354  nninfwlporlemd  7355  nninfwlporlem  7356  ofnegsub  9125  seqvalcd  10700  seq3feq2  10715  seq3feq  10719  seqf1oglem2  10759  seqfeq3  10768  ser0f  10773  facnn  10966  fac0  10967  resunimafz0  11071  wrdfn  11104  swrdvalfn  11209  pfxfn  11236  pfxid  11239  cats1un  11274  seq3shft  11370  fisumss  11924  prodf1f  12075  efcvgfsum  12199  nninfctlemfo  12582  ennnfonelemfun  13009  ennnfonelemf1  13010  prdsplusgsgrpcl  13468  prdssgrpd  13469  prdsplusgcl  13500  prdsidlem  13501  prdsmndd  13502  mhmf1o  13524  resmhm2b  13543  mhmima  13545  mhmeql  13546  gsumwmhm  13552  grpinvf1o  13624  prdsinvlem  13662  ghmrn  13815  ghmpreima  13824  ghmeql  13825  ghmnsgima  13826  ghmnsgpreima  13827  ghmeqker  13829  ghmf1o  13833  gsumfzmptfidmadd  13897  rhmf1o  14153  rnrhmsubrg  14237  psrbaglesuppg  14657  mplsubgfilemcl  14684  cnrest2  14931  lmss  14941  lmtopcnp  14945  upxp  14967  uptx  14969  cnmpt11  14978  cnmpt21  14986  cnmpt22f  14990  cnmptcom  14993  hmeof1o2  15003  psmetxrge0  15027  isxmet2d  15043  blelrnps  15114  blelrn  15115  xmetresbl  15135  comet  15194  bdxmet  15196  xmettx  15205  dvidlemap  15386  dvidrelem  15387  dvidsslem  15388  dvaddxxbr  15396  dvmulxxbr  15397  dvrecap  15408  plyaddlem1  15442  upgredg  15963  vtxedgfi  16075  vtxlpfi  16076  nninfall  16489  nninfsellemeqinf  16496  nninffeq  16500  nnnninfex  16502  nninfnfiinf  16503  refeq  16510