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∈V→AEB↔A∈B

Proof

Step Hyp Ref Expression
1 df-br ⊢AEB↔AB∈E
2 0nelopab ⊢¬∅∈xy|x∈y
3 df-eprel ⊢E=xy|x∈y
4 3 eqcomi ⊢xy|x∈y=E
5 4 eleq2i ⊢∅∈xy|x∈y↔∅∈E
6 2 5 mtbi ⊢¬∅∈E
7 eleq1 ⊢AB=∅→AB∈E↔∅∈E
8 6 7 mtbiri ⊢AB=∅→¬AB∈E
9 8 con2i ⊢AB∈E→¬AB=∅
10 opprc1 ⊢¬A∈V→AB=∅
11 9 10 nsyl2 ⊢AB∈E→A∈V
12 1 11 sylbi ⊢AEB→A∈V
13 12 a1i ⊢B∈V→AEB→A∈V
14 elex ⊢A∈B→A∈V
15 14 a1i ⊢B∈V→A∈B→A∈V
16 eleq12 ⊢x=A∧y=B→x∈y↔A∈B
17 16 3 brabga ⊢A∈V∧B∈V→AEB↔A∈B
18 17 expcom ⊢B∈V→A∈V→AEB↔A∈B
19 13 15 18 pm5.21ndd ⊢B∈V→AEB↔A∈B