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  12762  basmexd  12763  ismgmn0  13060  psrelbas  14304  psradd  14307  psraddcl  14308  istps  14352  topontopn  14357  cldrcl  14422  neiss2  14462