Theorem fnrel 5296

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

Syntax hints:   → wi 4  Rel wrel 4616  Fun wfun 5192   Fn wfn 5193

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

This theorem depends on definitions:  df-bi 116  df-fun 5200  df-fn 5201

This theorem is referenced by:  fnbr  5300  fnresdm  5307  fn0  5317  frel  5352  fcoi2  5379  f1rel  5407  f1ocnv  5455  dffn5im  5542  fnex  5718  fnexALT  6090  basmex  12474  basmexd  12475  ismgmn0  12612  istps  12824  topontopn  12829  cldrcl  12896  neiss2  12936