Metamath Proof Explorer

Theorem bj-epelb

Description: Two classes are related by the membership relation if and only if they are related by the membership relation (i.e., the first is an element of the second) and the second is a set (hence so is the first). TODO: move to Main after reordering to have brrelex2i available. Check if it is shorter to prove bj-epelg first or bj-epelb first. (Contributed by BJ, 14-Jul-2023)

Ref Expression
Assertion bj-epelb ⊢ A E B ↔ A ∈ B ∧ B ∈ V

Proof

Step Hyp Ref Expression
1 rele ⊢ Rel ⁡ E
2 1 brrelex2i ⊢ A E B → B ∈ V
3 2 pm4.71i ⊢ A E B ↔ A E B ∧ B ∈ V
4 epelg ⊢ B ∈ V → A E B ↔ A ∈ B
5 4 pm5.32ri ⊢ A E B ∧ B ∈ V ↔ A ∈ B ∧ B ∈ V
6 3 5 bitri ⊢ A E B ↔ A ∈ B ∧ B ∈ V