Theorem fnrel 5425

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

Syntax hints:   → wi 4  Rel wrel 4728  Fun wfun 5318   Fn wfn 5319

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 5326  df-fn 5327

This theorem is referenced by:  fnbr  5431  fnresdm  5438  fn0  5449  frel  5484  fcoi2  5515  f1rel  5543  f1ocnv  5593  dffn5im  5687  fnex  5871  fnexALT  6268  basmex  13135  basmexd  13136  ismgmn0  13434  psrelbas  14682  psradd  14686  psraddcl  14687  mplrcl  14701  mplbasss  14703  mpladd  14711  istps  14749  topontopn  14754  cldrcl  14819  neiss2  14859