Theorem fnrel 5377

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

Syntax hints:   → wi 4  Rel wrel 4684  Fun wfun 5270   Fn wfn 5271

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 5278  df-fn 5279

This theorem is referenced by:  fnbr  5383  fnresdm  5390  fn0  5401  frel  5436  fcoi2  5464  f1rel  5492  f1ocnv  5542  dffn5im  5631  fnex  5813  fnexALT  6203  basmex  12935  basmexd  12936  ismgmn0  13234  psrelbas  14481  psradd  14485  psraddcl  14486  mplrcl  14500  mplbasss  14502  mpladd  14510  istps  14548  topontopn  14553  cldrcl  14618  neiss2  14658