Description: Characterization of the elements of the powerclass of the cartesian square of the universal class: they are exactly the sets which are binary relations. (Contributed by BJ, 16-Dec-2023)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-pwvrelb | |- ( A e. ~P ( _V X. _V ) <-> ( A e. _V /\ Rel A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elex | |- ( A e. ~P ( _V X. _V ) -> A e. _V ) |
|
| 2 | pwvrel | |- ( A e. _V -> ( A e. ~P ( _V X. _V ) <-> Rel A ) ) |
|
| 3 | 1 2 | biadanii | |- ( A e. ~P ( _V X. _V ) <-> ( A e. _V /\ Rel A ) ) |