Description: The double converse of a class is a function iff the class is single-valued. Each side is equivalent to Definition 6.4(2) of TakeutiZaring p. 23, who use the notation "Un(A)" for single-valued. Note that A is not necessarily a function. (Contributed by NM, 13-Aug-2004)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | fun2cnv | |- ( Fun `' `' A <-> A. x E* y x A y ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | funcnv2 | |- ( Fun `' `' A <-> A. x E* y y `' A x ) |
|
| 2 | vex | |- y e. _V |
|
| 3 | vex | |- x e. _V |
|
| 4 | 2 3 | brcnv | |- ( y `' A x <-> x A y ) |
| 5 | 4 | mobii | |- ( E* y y `' A x <-> E* y x A y ) |
| 6 | 5 | albii | |- ( A. x E* y y `' A x <-> A. x E* y x A y ) |
| 7 | 1 6 | bitri | |- ( Fun `' `' A <-> A. x E* y x A y ) |