Theorem fnrel 6620

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

Syntax hints:   → wi 4  Rel wrel 5643  Fun wfun 6505   Fn wfn 6506

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 6513  df-fn 6514

This theorem is referenced by:  fnbr  6626  fnunres1  6630  fnresdm  6637  fn0  6649  frel  6693  fcoi2  6735  f1rel  6759  f1ocnv  6812  dffn5  6919  feqmptdf  6931  fconst5  7180  fnex  7191  fnexALT  7929  tz7.48-2  8410  resfnfinfin  9288  zorn2lem4  10452  imasvscafn  17500  2oppchomf  17685  opprabs  33453  bnj66  34850  tfsconcatb0  43333  tfsconcat0i  43334  tfsconcat0b  43335  tfsconcat00  43336  fnresdmss  45162  dfafn5a  47161  oppfvallem  49124  funcoppc3  49136  uptposlem  49186