Theorem fnrel 6594

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

Syntax hints:   → wi 4  Rel wrel 5630  Fun wfun 6486   Fn wfn 6487

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 208  df-an 397  df-fun 6494  df-fn 6495

This theorem is referenced by:  fnbr  6600  fnunres1  6604  fnresdm  6611  fn0  6623  frel  6667  fcoi2  6709  f1rel  6733  f1ocnv  6786  dffn5  6892  feqmptdf  6904  fconst5  7157  fnex  7168  fnexALT  7900  tz7.48-2  8378  resfnfinfin  9244  zorn2lem4  10419  imasvscafn  17499  2oppchomf  17688  fresunsn  32724  opprabs  33572  bnj66  35049  tfsconcatb0  43790  tfsconcat0i  43791  tfsconcat0b  43792  tfsconcat00  43793  fnresdmss  45616  dfafn5a  47624  oppfvallem  49626  funcoppc3  49638  uptposlem  49688