Theorem fnrel 5286

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

Syntax hints:   → wi 4  Rel wrel 4609  Fun wfun 5182   Fn wfn 5183

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 5190  df-fn 5191

This theorem is referenced by:  fnbr  5290  fnresdm  5297  fn0  5307  frel  5342  fcoi2  5369  f1rel  5397  f1ocnv  5445  dffn5im  5532  fnex  5707  fnexALT  6079  basmex  12452  ismgmn0  12589  istps  12680  topontopn  12685  cldrcl  12752  neiss2  12792