Theorem fnrel 6629

Description: A function with domain is a relation. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
fnrel	⊢ (𝐹 Fn 𝐴 → Rel 𝐹)

Proof of Theorem fnrel

Step	Hyp	Ref	Expression
1		fnfun 6627	. 2 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
2		funrel 6544	. 2 ⊢ (Fun 𝐹 → Rel 𝐹)
3	1, 2	syl 18	1 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)

This proof depends on syntax axioms:   → wi 4  Rel wrel 5652  Fun wfun 6521   Fn wfn 6522

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fun 6529  df-fn 6530

This theorem is used by:  fnbr  6635  fnunres1  6639  fnresdm  6646  fn0  6658  frel  6703  fcoi2  6745  f1relOLD  6771  f1ocnv  6825  dffn5  6931  feqmptdf  6943  fconst5  7200  fnex  7211  fnexALT  7946  tz7.48-2  8430  zorn2lem4  10549  imasvscafn  17671  2oppchomf  17860  opprabs  33940  bnj66  35425  tfsconcatb0  44289  tfsconcat0i  44290  tfsconcat0b  44291  tfsconcat00  44292  fnresdmss  46104  dfafn5a  48152  oppfvallem  50165  funcoppc3  50177  uptposlem  50227