Theorem fnrel 5459

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

Syntax hints:   → wi 4  Rel wrel 4759  Fun wfun 5351   Fn wfn 5352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117  df-fun 5359  df-fn 5360

This theorem is referenced by:  fnbr  5465  fnresdm  5472  fn0  5483  frel  5518  fcoi2  5553  f1rel  5582  f1ocnv  5632  dffn5im  5727  fnex  5911  fnexALT  6313  basmex  13359  basmexd  13360  ismgmn0  13624  psrelbas  14959  psradd  14963  psraddcl  14964  mplrcl  14978  mplbasss  14980  mpladd  14988  istps  15026  topontopn  15031  cldrcl  15096  neiss2  15136