Theorem fnrel 5428

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

Syntax hints:   → wi 4  Rel wrel 4730  Fun wfun 5320   Fn wfn 5321

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 5328  df-fn 5329

This theorem is referenced by:  fnbr  5434  fnresdm  5441  fn0  5452  frel  5487  fcoi2  5518  f1rel  5546  f1ocnv  5596  dffn5im  5691  fnex  5876  fnexALT  6273  basmex  13144  basmexd  13145  ismgmn0  13443  psrelbas  14692  psradd  14696  psraddcl  14697  mplrcl  14711  mplbasss  14713  mpladd  14721  istps  14759  topontopn  14764  cldrcl  14829  neiss2  14869