Theorem fnrel 5352

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

Syntax hints:   → wi 4  Rel wrel 4664  Fun wfun 5248   Fn wfn 5249

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 5256  df-fn 5257

This theorem is referenced by:  fnbr  5356  fnresdm  5363  fn0  5373  frel  5408  fcoi2  5435  f1rel  5463  f1ocnv  5513  dffn5im  5602  fnex  5780  fnexALT  6163  basmex  12677  basmexd  12678  ismgmn0  12941  psrelbas  14160  psradd  14163  psraddcl  14164  istps  14200  topontopn  14205  cldrcl  14270  neiss2  14310