Theorem funrel 2681

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 2432	. 2 ⊢ (Fun A ↔ (Rel A ∧ (A ∘ ◡A) ⊆ I))
2	1	pm3.26bd 259	1 ⊢ (Fun A → Rel A)

Syntax hints:   → wi 2   ⊆ wss 1487  Icid 2057  ^◡ccnv 2409   ∘ ccom 2414  Rel wrel 2415  Fun wfun 2416

This theorem is referenced by:  funss 2682  dffun7 2688  nfunv 2693  funssres 2698  funun 2700  fununi 2705  funimacnv 2711  fnrel 2722  f1orel 2803  funbrfv 2852  funfv2 2863  tfrlem6 2954  fundmen 3333

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

This theorem depends on definitions:  df-bi 128  df-an 198  df-fun 2432

metamath.org