Theorem fnrel 5315

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

Syntax hints:   → wi 4  Rel wrel 4632  Fun wfun 5211   Fn wfn 5212

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 5219  df-fn 5220

This theorem is referenced by:  fnbr  5319  fnresdm  5326  fn0  5336  frel  5371  fcoi2  5398  f1rel  5426  f1ocnv  5475  dffn5im  5562  fnex  5739  fnexALT  6112  basmex  12521  basmexd  12522  ismgmn0  12777  istps  13535  topontopn  13540  cldrcl  13605  neiss2  13645