Theorem fnrel 6601

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

Syntax hints:   → wi 4  Rel wrel 5636  Fun wfun 6493   Fn wfn 6494

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

This theorem is referenced by:  fnbr  6607  fnunres1  6611  fnresdm  6618  fn0  6630  frel  6674  fcoi2  6716  f1rel  6740  f1ocnv  6793  dffn5  6899  feqmptdf  6911  fconst5  7161  fnex  7172  fnexALT  7904  tz7.48-2  8381  resfnfinfin  9247  zorn2lem4  10421  imasvscafn  17501  2oppchomf  17690  fresunsn  32698  opprabs  33542  bnj66  35002  tfsconcatb0  43772  tfsconcat0i  43773  tfsconcat0b  43774  tfsconcat00  43775  fnresdmss  45598  dfafn5a  47602  oppfvallem  49604  funcoppc3  49616  uptposlem  49666