Theorem fnrel 6602

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

Syntax hints:   → wi 4  Rel wrel 5637  Fun wfun 6494   Fn wfn 6495

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 6502  df-fn 6503

This theorem is referenced by:  fnbr  6608  fnunres1  6612  fnresdm  6619  fn0  6631  frel  6675  fcoi2  6717  f1rel  6741  f1ocnv  6794  dffn5  6900  feqmptdf  6912  fconst5  7162  fnex  7173  fnexALT  7905  tz7.48-2  8383  resfnfinfin  9249  zorn2lem4  10421  imasvscafn  17470  2oppchomf  17659  fresunsn  32714  opprabs  33574  bnj66  35035  tfsconcatb0  43690  tfsconcat0i  43691  tfsconcat0b  43692  tfsconcat00  43693  fnresdmss  45516  dfafn5a  47509  oppfvallem  49483  funcoppc3  49495  uptposlem  49545