Theorem fnrel 5326

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

Syntax hints:   → wi 4  Rel wrel 4643  Fun wfun 5222   Fn wfn 5223

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 5230  df-fn 5231

This theorem is referenced by:  fnbr  5330  fnresdm  5337  fn0  5347  frel  5382  fcoi2  5409  f1rel  5437  f1ocnv  5486  dffn5im  5574  fnex  5751  fnexALT  6126  basmex  12535  basmexd  12536  ismgmn0  12796  istps  13885  topontopn  13890  cldrcl  13955  neiss2  13995