Theorem fnrel 5419

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

Syntax hints:   → wi 4  Rel wrel 4724  Fun wfun 5312   Fn wfn 5313

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 5320  df-fn 5321

This theorem is referenced by:  fnbr  5425  fnresdm  5432  fn0  5443  frel  5478  fcoi2  5509  f1rel  5537  f1ocnv  5587  dffn5im  5681  fnex  5865  fnexALT  6262  basmex  13100  basmexd  13101  ismgmn0  13399  psrelbas  14647  psradd  14651  psraddcl  14652  mplrcl  14666  mplbasss  14668  mpladd  14676  istps  14714  topontopn  14719  cldrcl  14784  neiss2  14824