Theorem fnrel 5479

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

This proof depends on syntax axioms:   → wi 4  Rel wrel 4779  Fun wfun 5371   Fn wfn 5372

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-fun 5379  df-fn 5380

This theorem is used by:  fnbr  5485  fnresdm  5492  fn0  5503  frel  5538  fcoi2  5573  f1rel  5602  f1ocnv  5652  dffn5im  5748  fnex  5937  fnexALT  6340  basmex  13414  basmexd  13415  slotm  13417  ismgmn0  13680  mgpplusg  14224  mgpbas  14227  ringidval  14267  psrelbas  15068  psradd  15072  psraddcl  15073  mplrcl  15087  mplbasss  15089  mpladd  15097  istps  15135  topontopn  15140  cldrcl  15205  neiss2  15245