Theorem fnrel 6591

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

Syntax hints:   → wi 4  Rel wrel 5626  Fun wfun 6483   Fn wfn 6484

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 6491  df-fn 6492

This theorem is referenced by:  fnbr  6597  fnunres1  6601  fnresdm  6608  fn0  6620  frel  6664  fcoi2  6706  f1rel  6730  f1ocnv  6783  dffn5  6889  feqmptdf  6901  fconst5  7149  fnex  7160  fnexALT  7892  tz7.48-2  8370  resfnfinfin  9231  zorn2lem4  10400  imasvscafn  17451  2oppchomf  17640  opprabs  33458  bnj66  34883  tfsconcatb0  43451  tfsconcat0i  43452  tfsconcat0b  43453  tfsconcat00  43454  fnresdmss  45279  dfafn5a  47274  oppfvallem  49250  funcoppc3  49262  uptposlem  49312