Theorem fnrel 5456

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

Syntax hints:   → wi 4  Rel wrel 4756  Fun wfun 5348   Fn wfn 5349

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 5356  df-fn 5357

This theorem is referenced by:  fnbr  5462  fnresdm  5469  fn0  5480  frel  5515  fcoi2  5550  f1rel  5579  f1ocnv  5629  dffn5im  5724  fnex  5908  fnexALT  6306  basmex  13293  basmexd  13294  ismgmn0  13592  psrelbas  14879  psradd  14883  psraddcl  14884  mplrcl  14898  mplbasss  14900  mpladd  14908  istps  14946  topontopn  14951  cldrcl  15016  neiss2  15056