Theorem fnrel 5453

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

Syntax hints:   → wi 4  Rel wrel 4753  Fun wfun 5345   Fn wfn 5346

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 5353  df-fn 5354

This theorem is referenced by:  fnbr  5459  fnresdm  5466  fn0  5477  frel  5512  fcoi2  5547  f1rel  5576  f1ocnv  5626  dffn5im  5721  fnex  5905  fnexALT  6303  basmex  13261  basmexd  13262  ismgmn0  13560  psrelbas  14817  psradd  14821  psraddcl  14822  mplrcl  14836  mplbasss  14838  mpladd  14846  istps  14884  topontopn  14889  cldrcl  14954  neiss2  14994