Metamath Proof Explorer


Theorem epelg

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) (Proof shortened by BJ, 14-Jul-2023)

Ref Expression
Assertion epelg
|- ( B e. V -> ( A _E B <-> A e. B ) )

Proof

Step Hyp Ref Expression
1 df-br
 |-  ( A _E B <-> <. A , B >. e. _E )
2 0nelopab
 |-  -. (/) e. { <. x , y >. | x e. y }
3 df-eprel
 |-  _E = { <. x , y >. | x e. y }
4 3 eqcomi
 |-  { <. x , y >. | x e. y } = _E
5 4 eleq2i
 |-  ( (/) e. { <. x , y >. | x e. y } <-> (/) e. _E )
6 2 5 mtbi
 |-  -. (/) e. _E
7 eleq1
 |-  ( <. A , B >. = (/) -> ( <. A , B >. e. _E <-> (/) e. _E ) )
8 6 7 mtbiri
 |-  ( <. A , B >. = (/) -> -. <. A , B >. e. _E )
9 8 con2i
 |-  ( <. A , B >. e. _E -> -. <. A , B >. = (/) )
10 opprc1
 |-  ( -. A e. _V -> <. A , B >. = (/) )
11 9 10 nsyl2
 |-  ( <. A , B >. e. _E -> A e. _V )
12 1 11 sylbi
 |-  ( A _E B -> A e. _V )
13 12 a1i
 |-  ( B e. V -> ( A _E B -> A e. _V ) )
14 elex
 |-  ( A e. B -> A e. _V )
15 14 a1i
 |-  ( B e. V -> ( A e. B -> A e. _V ) )
16 eleq12
 |-  ( ( x = A /\ y = B ) -> ( x e. y <-> A e. B ) )
17 16 3 brabga
 |-  ( ( A e. _V /\ B e. V ) -> ( A _E B <-> A e. B ) )
18 17 expcom
 |-  ( B e. V -> ( A e. _V -> ( A _E B <-> A e. B ) ) )
19 13 15 18 pm5.21ndd
 |-  ( B e. V -> ( A _E B <-> A e. B ) )