Theorem fnrel 5422

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

Syntax hints:   → wi 4  Rel wrel 4725  Fun wfun 5315   Fn wfn 5316

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 5323  df-fn 5324

This theorem is referenced by:  fnbr  5428  fnresdm  5435  fn0  5446  frel  5481  fcoi2  5512  f1rel  5540  f1ocnv  5590  dffn5im  5684  fnex  5868  fnexALT  6265  basmex  13113  basmexd  13114  ismgmn0  13412  psrelbas  14660  psradd  14664  psraddcl  14665  mplrcl  14679  mplbasss  14681  mpladd  14689  istps  14727  topontopn  14732  cldrcl  14797  neiss2  14837