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	⊢ ( 𝐴 E 𝐵 ↔ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ V ) )

Proof

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