This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 . Definition 1.6 of Schloeder p. 1. (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 ) )