Theorem frel 3644

Description: A mapping is a relation.

Assertion

Ref	Expression
frel	⊢ (F:A–→B → Rel F)

Proof of Theorem frel

Step	Hyp	Ref	Expression
1		ffn 3641	. 2 ⊢ (F:A–→B → F Fn A)
2		fnrel 3600	. 2 ⊢ (F Fn A → Rel F)
3	1, 2	syl 10	1 ⊢ (F:A–→B → Rel F)

Syntax hints:   → wi 3  Rel wrel 3189   Fn wfn 3191  –→wf 3192

This theorem is referenced by:  fssxp 3651  fcoi2 3660  foconst 3697  fsn 3848  mapsn 4359  metne0 7830  hmeobc 10548

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 3206  df-fn 3207  df-f 3208

Copyright terms: Public domain