Description: Two classes are related by the membership relation if and only if they are related by the membership relation (i.e., the first is an element of the second) and the second is a set (hence so is the first). TODO: move to Main after reordering to have brrelex2i available. Check if it is shorter to prove bj-epelg first or bj-epelb first. (Contributed by BJ, 14-Jul-2023)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-epelb | |- ( A _E B <-> ( A e. B /\ B e. _V ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rele | |- Rel _E |
|
| 2 | 1 | brrelex2i | |- ( A _E B -> B e. _V ) |
| 3 | 2 | pm4.71i | |- ( A _E B <-> ( A _E B /\ B e. _V ) ) |
| 4 | epelg | |- ( B e. _V -> ( A _E B <-> A e. B ) ) |
|
| 5 | 4 | pm5.32ri | |- ( ( A _E B /\ B e. _V ) <-> ( A e. B /\ B e. _V ) ) |
| 6 | 3 5 | bitri | |- ( A _E B <-> ( A e. B /\ B e. _V ) ) |