Theorem epelgOLD

Description: Obsolete version of epelg as of 14-Jul-2023. (Contributed by Scott Fenton, 27-Mar-2011) (Revised by Mario Carneiro, 28-Apr-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	epelgOLD	$$⊢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		elopab	$$⊢⟨A,B⟩\in \left\{⟨x,y⟩|x\in y\right\}\leftrightarrow \exists x\exists y\left(⟨A,B⟩=⟨x,y⟩\wedge x\in y\right)$$
3		vex	$$⊢x\in \mathrm{V}$$
4		vex	$$⊢y\in \mathrm{V}$$
5	3 4	pm3.2i	$$⊢\left(x\in \mathrm{V}\wedge y\in \mathrm{V}\right)$$
6		opeqex	$$⊢⟨A,B⟩=⟨x,y⟩\to \left(\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\leftrightarrow \left(x\in \mathrm{V}\wedge y\in \mathrm{V}\right)\right)$$
7	5 6	mpbiri	$$⊢⟨A,B⟩=⟨x,y⟩\to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$
8	7	simpld	$$⊢⟨A,B⟩=⟨x,y⟩\to A\in \mathrm{V}$$
9	8	adantr	$$⊢\left(⟨A,B⟩=⟨x,y⟩\wedge x\in y\right)\to A\in \mathrm{V}$$
10	9	exlimivv	$$⊢\exists x\exists y\left(⟨A,B⟩=⟨x,y⟩\wedge x\in y\right)\to A\in \mathrm{V}$$
11	2 10	sylbi	$$⊢⟨A,B⟩\in \left\{⟨x,y⟩|x\in y\right\}\to A\in \mathrm{V}$$
12		df-eprel	$$⊢\mathrm{E}=\left\{⟨x,y⟩|x\in y\right\}$$
13	11 12	eleq2s	$$⊢⟨A,B⟩\in \mathrm{E}\to A\in \mathrm{V}$$
14	1 13	sylbi	$$⊢A\mathrm{E}B\to A\in \mathrm{V}$$
15	14	a1i	$$⊢B\in V\to \left(A\mathrm{E}B\to A\in \mathrm{V}\right)$$
16		elex	$$⊢A\in B\to A\in \mathrm{V}$$
17	16	a1i	$$⊢B\in V\to \left(A\in B\to A\in \mathrm{V}\right)$$
18		eleq12	$$⊢\left(x=A\wedge y=B\right)\to \left(x\in y\leftrightarrow A\in B\right)$$
19	18 12	brabga	$$⊢\left(A\in \mathrm{V}\wedge B\in V\right)\to \left(A\mathrm{E}B\leftrightarrow A\in B\right)$$
20	19	expcom	$$⊢B\in V\to \left(A\in \mathrm{V}\to \left(A\mathrm{E}B\leftrightarrow A\in B\right)\right)$$
21	15 17 20	pm5.21ndd	$$⊢B\in V\to \left(A\mathrm{E}B\leftrightarrow A\in B\right)$$