Theorem fnrel 5482

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

This proof depends on syntax axioms:   → wi 4  Rel wrel 4781  Fun wfun 5374   Fn wfn 5375

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 5382  df-fn 5383

This theorem is used by:  fnbr  5488  fnresdm  5495  fn0  5506  frel  5541  fcoi2  5576  f1rel  5605  f1ocnv  5655  dffn5im  5751  fnex  5940  fnexALT  6344  basmex  13471  basmexd  13472  slotm  13474  ismgmn0  13738  mgpplusg  14330  mgpbas  14333  ringidval  14373  psrelbas  15184  psradd  15188  psraddcl  15189  psrmulfval  15192  mplrcl  15222  mplbasss  15224  mpladd  15232  istps  15270  topontopn  15275  cldrcl  15340  neiss2  15380