Theorem fnrel 5357

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

Syntax hints:   → wi 4  Rel wrel 4669  Fun wfun 5253   Fn wfn 5254

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 5261  df-fn 5262

This theorem is referenced by:  fnbr  5363  fnresdm  5370  fn0  5380  frel  5415  fcoi2  5442  f1rel  5470  f1ocnv  5520  dffn5im  5609  fnex  5787  fnexALT  6177  basmex  12764  basmexd  12765  ismgmn0  13062  psrelbas  14309  psradd  14313  psraddcl  14314  mplrcl  14328  mplbasss  14330  mpladd  14338  istps  14376  topontopn  14381  cldrcl  14446  neiss2  14486