Theorem fnrel 6588

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

Syntax hints:   → wi 4  Rel wrel 5628  Fun wfun 6480   Fn wfn 6481

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 6488  df-fn 6489

This theorem is referenced by:  fnbr  6594  fnunres1  6598  fnresdm  6605  fn0  6617  frel  6661  fcoi2  6703  f1rel  6727  f1ocnv  6780  dffn5  6885  feqmptdf  6897  fconst5  7146  fnex  7157  fnexALT  7893  tz7.48-2  8371  resfnfinfin  9246  zorn2lem4  10412  imasvscafn  17459  2oppchomf  17648  opprabs  33429  bnj66  34826  tfsconcatb0  43317  tfsconcat0i  43318  tfsconcat0b  43319  tfsconcat00  43320  fnresdmss  45146  dfafn5a  47145  oppfvallem  49108  funcoppc3  49120  uptposlem  49170