Theorem fnrel 6595

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

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

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 6495  df-fn 6496

This theorem is referenced by:  fnbr  6601  fnunres1  6605  fnresdm  6612  fn0  6624  frel  6668  fcoi2  6710  f1rel  6734  f1ocnv  6787  dffn5  6893  feqmptdf  6905  fconst5  7154  fnex  7165  fnexALT  7897  tz7.48-2  8375  resfnfinfin  9241  zorn2lem4  10413  imasvscafn  17462  2oppchomf  17651  fresunsn  32685  opprabs  33544  bnj66  34997  tfsconcatb0  43622  tfsconcat0i  43623  tfsconcat0b  43624  tfsconcat00  43625  fnresdmss  45448  dfafn5a  47442  oppfvallem  49416  funcoppc3  49428  uptposlem  49478