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 ) )