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  14306  psradd  14309  psraddcl  14310  istps  14354  topontopn  14359  cldrcl  14424  neiss2  14464