Metamath Proof Explorer

Theorem bj-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) TODO: move it to the main section after reordering to have brrelex1i available. (Proof shortened by BJ, 14-Jul-2023) (Proof modification is discouraged.)

Ref Expression
Assertion bj-epelg ⊢ B ∈ V → A E B ↔ A ∈ B

Proof

Step Hyp Ref Expression
1 rele ⊢ Rel ⁡ E
2 1 brrelex1i ⊢ A E B → A ∈ V
3 2 a1i ⊢ B ∈ V → A E B → A ∈ V
4 elex ⊢ A ∈ B → A ∈ V
5 4 a1i ⊢ B ∈ V → A ∈ B → A ∈ V
6 eleq12 ⊢ x = A ∧ y = B → x ∈ y ↔ A ∈ B
7 df-eprel ⊢ E = x y | x ∈ y
8 6 7 brabga ⊢ A ∈ V ∧ B ∈ V → A E B ↔ A ∈ B
9 8 expcom ⊢ B ∈ V → A ∈ V → A E B ↔ A ∈ B
10 3 5 9 pm5.21ndd ⊢ B ∈ V → A E B ↔ A ∈ B