Description: The coordinates of an ordered pair that belongs to a relation are sets. TODO: Slightly shorter than brrelex12 , which could be proved from it. (Contributed by BJ, 27-Dec-2023)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-opelrelex | |- ( ( Rel R /\ <. A , B >. e. R ) -> ( A e. _V /\ B e. _V ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-rel | |- ( Rel R <-> R C_ ( _V X. _V ) ) |
|
| 2 | 1 | biimpi | |- ( Rel R -> R C_ ( _V X. _V ) ) |
| 3 | 2 | sselda | |- ( ( Rel R /\ <. A , B >. e. R ) -> <. A , B >. e. ( _V X. _V ) ) |
| 4 | opelxp | |- ( <. A , B >. e. ( _V X. _V ) <-> ( A e. _V /\ B e. _V ) ) |
|
| 5 | 3 4 | sylib | |- ( ( Rel R /\ <. A , B >. e. R ) -> ( A e. _V /\ B e. _V ) ) |