Theorem fnrel 5482

Description: A function with domain is a relation. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
fnrel	|- ( F Fn A -> Rel F )

Proof of Theorem fnrel

Step	Hyp	Ref	Expression
1		fnfun 5481	. 2 |- ( F Fn A -> Fun F )
2		funrel 5397	. 2 |- ( Fun F -> Rel F )
3	1, 2	syl 14	1 |- ( F Fn A -> Rel F )

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  13470  basmexd  13471  slotm  13473  ismgmn0  13737  mgpplusg  14329  mgpbas  14332  ringidval  14372  psrelbas  15179  psradd  15183  psraddcl  15184  psrmulfval  15187  mplrcl  15210  mplbasss  15212  mpladd  15220  istps  15258  topontopn  15263  cldrcl  15328  neiss2  15368