Theorem fnrel 5356

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

Syntax hints:   → wi 4  Rel wrel 4668  Fun wfun 5252   Fn wfn 5253

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 5260  df-fn 5261

This theorem is referenced by:  fnbr  5360  fnresdm  5367  fn0  5377  frel  5412  fcoi2  5439  f1rel  5467  f1ocnv  5517  dffn5im  5606  fnex  5784  fnexALT  6168  basmex  12737  basmexd  12738  ismgmn0  13001  psrelbas  14228  psradd  14231  psraddcl  14232  istps  14268  topontopn  14273  cldrcl  14338  neiss2  14378