Description: If two classes are related by a binary relation, then the first class is a set. (Contributed by NM, 18-May-2004) (Revised by Mario Carneiro, 26-Apr-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | brrelex1 | |- ( ( Rel R /\ A R B ) -> A e. _V ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | brrelex12 | |- ( ( Rel R /\ A R B ) -> ( A e. _V /\ B e. _V ) ) |
|
| 2 | 1 | simpld | |- ( ( Rel R /\ A R B ) -> A e. _V ) |