Description: The membership relation and the membership predicate agree when the "containing" class is a set. General version of epel and closed form of epeli . (Contributed by Scott Fenton, 27-Mar-2011) (Revised by Mario Carneiro, 28-Apr-2015) TODO: move it to the main section after reordering to have brrelex1i available. (Proof shortened by BJ, 14-Jul-2023) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-epelg | |- ( B e. V -> ( A _E B <-> A e. B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rele | |- Rel _E |
|
| 2 | 1 | brrelex1i | |- ( A _E B -> A e. _V ) |
| 3 | 2 | a1i | |- ( B e. V -> ( A _E B -> A e. _V ) ) |
| 4 | elex | |- ( A e. B -> A e. _V ) |
|
| 5 | 4 | a1i | |- ( B e. V -> ( A e. B -> A e. _V ) ) |
| 6 | eleq12 | |- ( ( x = A /\ y = B ) -> ( x e. y <-> A e. B ) ) |
|
| 7 | df-eprel | |- _E = { <. x , y >. | x e. y } |
|
| 8 | 6 7 | brabga | |- ( ( A e. _V /\ B e. V ) -> ( A _E B <-> A e. B ) ) |
| 9 | 8 | expcom | |- ( B e. V -> ( A e. _V -> ( A _E B <-> A e. B ) ) ) |
| 10 | 3 5 9 | pm5.21ndd | |- ( B e. V -> ( A _E B <-> A e. B ) ) |