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  13289  basmexd  13290  ismgmn0  13588  psrelbas  14847  psradd  14851  psraddcl  14852  mplrcl  14866  mplbasss  14868  mpladd  14876  istps  14914  topontopn  14919  cldrcl  14984  neiss2  15024