Theorem fnrel 5353

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

Syntax hints:   → wi 4  Rel wrel 4665  Fun wfun 5249   Fn wfn 5250

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 5257  df-fn 5258

This theorem is referenced by:  fnbr  5357  fnresdm  5364  fn0  5374  frel  5409  fcoi2  5436  f1rel  5464  f1ocnv  5514  dffn5im  5603  fnex  5781  fnexALT  6165  basmex  12680  basmexd  12681  ismgmn0  12944  psrelbas  14171  psradd  14174  psraddcl  14175  istps  14211  topontopn  14216  cldrcl  14281  neiss2  14321