Theorem funrel 3533

Description: A function is a relation.

Assertion

Ref	Expression
funrel	|- (Fun A -> Rel A)

Proof of Theorem funrel

Step	Hyp	Ref	Expression
1		df-fun 3192	. 2 |- (Fun A <-> (Rel A /\ (A o. `'A) (_ I))
2	1	pm3.26bi 322	1 |- (Fun A -> Rel A)

Syntax hints:   -> wi 3   (_ wss 2047  Icid 2831  `'ccnv 3169   o. ccom 3174  Rel wrel 3175  Fun wfun 3176

This theorem is referenced by:  funss 3534  dffun7 3540  nfunv 3546  funopg 3547  funssres 3552  funun 3554  fununi 3563  funcnvres2 3570  fnrel 3586  f1orel 3692  funbrfv 3750  funfv2 3771  tfrlem6 3916  fundmen 4428

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-fun 3192

Copyright terms: Public domain