Theorem funrel 3529

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 3188	. 2 |- (Fun A <-> (Rel A /\ (A o. `'A) (_ I))
2	1	pm3.26bi 322	1 |- (Fun A -> Rel A)

Syntax hints:   -> wi 3   (_ wss 2044  Icid 2827  `'ccnv 3165   o. ccom 3170  Rel wrel 3171  Fun wfun 3172

This theorem is referenced by:  funss 3530  dffun7 3536  nfunv 3542  funopg 3543  funssres 3548  funun 3550  fununi 3559  funcnvres2 3566  fnrel 3582  f1orel 3687  funbrfv 3745  funfv2 3766  tfrlem6 3911  fundmen 4418

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 3188

Copyright terms: Public domain