Theorem fnrel 6579

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

Syntax hints:   → wi 4  Rel wrel 5619  Fun wfun 6471   Fn wfn 6472

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 6479  df-fn 6480

This theorem is referenced by:  fnbr  6585  fnunres1  6589  fnresdm  6596  fn0  6608  frel  6652  fcoi2  6694  f1rel  6718  f1ocnv  6771  dffn5  6875  feqmptdf  6887  fconst5  7135  fnex  7146  fnexALT  7878  tz7.48-2  8356  resfnfinfin  9216  zorn2lem4  10382  imasvscafn  17433  2oppchomf  17622  opprabs  33437  bnj66  34862  tfsconcatb0  43356  tfsconcat0i  43357  tfsconcat0b  43358  tfsconcat00  43359  fnresdmss  45184  dfafn5a  47170  oppfvallem  49146  funcoppc3  49158  uptposlem  49208