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

Proof

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