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

Proof

Step	Hyp	Ref	Expression
1		df-br	$$⊢A\mathrm{E}B\leftrightarrow ⟨A,B⟩\in \mathrm{E}$$
2		0nelopab	$$⊢\neg \varnothing \in \left\{⟨x,y⟩|x\in y\right\}$$
3		df-eprel	$$⊢\mathrm{E}=\left\{⟨x,y⟩|x\in y\right\}$$
4	3	eqcomi	$$⊢\left\{⟨x,y⟩|x\in y\right\}=\mathrm{E}$$
5	4	eleq2i	$$⊢\varnothing \in \left\{⟨x,y⟩|x\in y\right\}\leftrightarrow \varnothing \in \mathrm{E}$$
6	2 5	mtbi	$$⊢\neg \varnothing \in \mathrm{E}$$
7		eleq1	$$⊢⟨A,B⟩=\varnothing \to \left(⟨A,B⟩\in \mathrm{E}\leftrightarrow \varnothing \in \mathrm{E}\right)$$
8	6 7	mtbiri	$$⊢⟨A,B⟩=\varnothing \to \neg ⟨A,B⟩\in \mathrm{E}$$
9	8	con2i	$$⊢⟨A,B⟩\in \mathrm{E}\to \neg ⟨A,B⟩=\varnothing$$
10		opprc1	$$⊢\neg A\in \mathrm{V}\to ⟨A,B⟩=\varnothing$$
11	9 10	nsyl2	$$⊢⟨A,B⟩\in \mathrm{E}\to A\in \mathrm{V}$$
12	1 11	sylbi	$$⊢A\mathrm{E}B\to A\in \mathrm{V}$$
13	12	a1i	$$⊢B\in V\to \left(A\mathrm{E}B\to A\in \mathrm{V}\right)$$
14		elex	$$⊢A\in B\to A\in \mathrm{V}$$
15	14	a1i	$$⊢B\in V\to \left(A\in B\to A\in \mathrm{V}\right)$$
16		eleq12	$$⊢\left(x=A\wedge y=B\right)\to \left(x\in y\leftrightarrow A\in B\right)$$
17	16 3	brabga	$$⊢\left(A\in \mathrm{V}\wedge B\in V\right)\to \left(A\mathrm{E}B\leftrightarrow A\in B\right)$$
18	17	expcom	$$⊢B\in V\to \left(A\in \mathrm{V}\to \left(A\mathrm{E}B\leftrightarrow A\in B\right)\right)$$
19	13 15 18	pm5.21ndd	$$⊢B\in V\to \left(A\mathrm{E}B\leftrightarrow A\in B\right)$$