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\in V\to \left(A\mathrm{E}B\leftrightarrow A\in B\right)$$

Proof

Step	Hyp	Ref	Expression
1		rele	$$⊢\mathrm{Rel}\mathrm{E}$$
2	1	brrelex1i	$$⊢A\mathrm{E}B\to A\in \mathrm{V}$$
3	2	a1i	$$⊢B\in V\to \left(A\mathrm{E}B\to A\in \mathrm{V}\right)$$
4		elex	$$⊢A\in B\to A\in \mathrm{V}$$
5	4	a1i	$$⊢B\in V\to \left(A\in B\to A\in \mathrm{V}\right)$$
6		eleq12	$$⊢\left(x=A\wedge y=B\right)\to \left(x\in y\leftrightarrow A\in B\right)$$
7		df-eprel	$$⊢\mathrm{E}=\left\{⟨x,y⟩|x\in y\right\}$$
8	6 7	brabga	$$⊢\left(A\in \mathrm{V}\wedge B\in V\right)\to \left(A\mathrm{E}B\leftrightarrow A\in B\right)$$
9	8	expcom	$$⊢B\in V\to \left(A\in \mathrm{V}\to \left(A\mathrm{E}B\leftrightarrow A\in B\right)\right)$$
10	3 5 9	pm5.21ndd	$$⊢B\in V\to \left(A\mathrm{E}B\leftrightarrow A\in B\right)$$