Theorem fnrel 5395

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

Syntax hints:   → wi 4  Rel wrel 4701  Fun wfun 5288   Fn wfn 5289

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 5296  df-fn 5297

This theorem is referenced by:  fnbr  5401  fnresdm  5408  fn0  5419  frel  5454  fcoi2  5483  f1rel  5511  f1ocnv  5561  dffn5im  5652  fnex  5834  fnexALT  6226  basmex  13058  basmexd  13059  ismgmn0  13357  psrelbas  14604  psradd  14608  psraddcl  14609  mplrcl  14623  mplbasss  14625  mpladd  14633  istps  14671  topontopn  14676  cldrcl  14741  neiss2  14781