Description: A single-valued relation is a function. (See fun2cnv for "single-valued.") Definition 6.4(4) of TakeutiZaring p. 24. (Contributed by NM, 17-Jan-2006)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | svrelfun | |- ( Fun A <-> ( Rel A /\ Fun `' `' A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dffun6 | |- ( Fun A <-> ( Rel A /\ A. x E* y x A y ) ) |
|
| 2 | fun2cnv | |- ( Fun `' `' A <-> A. x E* y x A y ) |
|
| 3 | 2 | anbi2i | |- ( ( Rel A /\ Fun `' `' A ) <-> ( Rel A /\ A. x E* y x A y ) ) |
| 4 | 1 3 | bitr4i | |- ( Fun A <-> ( Rel A /\ Fun `' `' A ) ) |