Theorem fnrel 5477

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

Syntax hints:   → wi 4  Rel wrel 4777  Fun wfun 5369   Fn wfn 5370

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 5377  df-fn 5378

This theorem is referenced by:  fnbr  5483  fnresdm  5490  fn0  5501  frel  5536  fcoi2  5571  f1rel  5600  f1ocnv  5650  dffn5im  5745  fnex  5931  fnexALT  6334  basmex  13395  basmexd  13396  slotm  13398  ismgmn0  13661  mgpplusg  14205  mgpbas  14208  ringidval  14248  psrelbas  15049  psradd  15053  psraddcl  15054  mplrcl  15068  mplbasss  15070  mpladd  15078  istps  15116  topontopn  15121  cldrcl  15186  neiss2  15226