Theorem fnrel 6592

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 6590	. 2 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
2		funrel 6507	. 2 ⊢ (Fun 𝐹 → Rel 𝐹)
3	1, 2	syl 17	1 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)

Syntax hints:   → wi 4  Rel wrel 5627  Fun wfun 6484   Fn wfn 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-fun 6492  df-fn 6493

This theorem is referenced by:  fnbr  6598  fnunres1  6602  fnresdm  6609  fn0  6621  frel  6665  fcoi2  6707  f1rel  6731  f1ocnv  6784  dffn5  6890  feqmptdf  6902  fconst5  7152  fnex  7163  fnexALT  7895  tz7.48-2  8372  resfnfinfin  9238  zorn2lem4  10410  imasvscafn  17490  2oppchomf  17679  fresunsn  32718  opprabs  33562  bnj66  35023  tfsconcatb0  43787  tfsconcat0i  43788  tfsconcat0b  43789  tfsconcat00  43790  fnresdmss  45613  dfafn5a  47605  oppfvallem  49607  funcoppc3  49619  uptposlem  49669