Theorem fnrel 6612

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

Syntax hints:   → wi 4  Rel wrel 5645  Fun wfun 6504   Fn wfn 6505

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 209  df-an 399  df-fun 6512  df-fn 6513

This theorem is referenced by:  fnbr  6618  fnunres1  6622  fnresdm  6629  fn0  6641  frel  6686  fcoi2  6728  f1relOLD  6754  f1ocnv  6808  dffn5  6914  feqmptdf  6926  fconst5  7179  fnex  7190  fnexALT  7921  tz7.48-2  8401  resfnfinfin  9270  zorn2lem4  10446  imasvscafn  17543  2oppchomf  17732  fresunsn  32770  opprabs  33624  bnj66  35112  tfsconcatb0  43869  tfsconcat0i  43870  tfsconcat0b  43871  tfsconcat00  43872  fnresdmss  45694  dfafn5a  47702  oppfvallem  49704  funcoppc3  49716  uptposlem  49766