Theorem fnrel 5430

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

Syntax hints:   → wi 4  Rel wrel 4732  Fun wfun 5322   Fn wfn 5323

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 5330  df-fn 5331

This theorem is referenced by:  fnbr  5436  fnresdm  5443  fn0  5454  frel  5489  fcoi2  5520  f1rel  5549  f1ocnv  5599  dffn5im  5694  fnex  5879  fnexALT  6278  basmex  13165  basmexd  13166  ismgmn0  13464  psrelbas  14718  psradd  14722  psraddcl  14723  mplrcl  14737  mplbasss  14739  mpladd  14747  istps  14785  topontopn  14790  cldrcl  14855  neiss2  14895