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  13469  basmexd  13470  slotm  13472  ismgmn0  13736  mgpplusg  14328  mgpbas  14331  ringidval  14371  psrelbas  15188  psradd  15192  psraddcl  15193  psrmulfval  15196  mplbas  15223  mplrcl  15227  mpladd  15237  istps  15275  topontopn  15280  cldrcl  15345  neiss2  15385