Theorem eu2ndop1stv

Description: If there is a unique second component in an ordered pair contained in a given set, the first component must be a set. (Contributed by Alexander van der Vekens, 29-Nov-2017)

	Ref	Expression
Assertion	eu2ndop1stv	$$⊢\exists !y⟨A,y⟩\in V\to A\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		euex	$$⊢\exists !y⟨A,y⟩\in V\to \exists y⟨A,y⟩\in V$$
2		nfeu1	$$⊢Ⅎy\exists !y⟨A,y⟩\in V$$
3		nfcv	$$⊢\underset{\_}{Ⅎ}yA$$
4	3	nfel1	$$⊢ℲyA\in \mathrm{V}$$
5	2 4	nfim	$$⊢Ⅎy\left(\exists !y⟨A,y⟩\in V\to A\in \mathrm{V}\right)$$
6		opprc1	$$⊢\neg A\in \mathrm{V}\to ⟨A,y⟩=\varnothing$$
7	6	eleq1d	$$⊢\neg A\in \mathrm{V}\to \left(⟨A,y⟩\in V\leftrightarrow \varnothing \in V\right)$$
8		ax-5	$$⊢\varnothing \in V\to \forall y\varnothing \in V$$
9		alneu	$$⊢\forall y\varnothing \in V\to \neg \exists !y\varnothing \in V$$
10	8 9	syl	$$⊢\varnothing \in V\to \neg \exists !y\varnothing \in V$$
11	7 10	biimtrdi	$$⊢\neg A\in \mathrm{V}\to \left(⟨A,y⟩\in V\to \neg \exists !y\varnothing \in V\right)$$
12	11	impcom	$$⊢\left(⟨A,y⟩\in V\wedge \neg A\in \mathrm{V}\right)\to \neg \exists !y\varnothing \in V$$
13	7	eubidv	$$⊢\neg A\in \mathrm{V}\to \left(\exists !y⟨A,y⟩\in V\leftrightarrow \exists !y\varnothing \in V\right)$$
14	13	notbid	$$⊢\neg A\in \mathrm{V}\to \left(\neg \exists !y⟨A,y⟩\in V\leftrightarrow \neg \exists !y\varnothing \in V\right)$$
15	14	adantl	$$⊢\left(⟨A,y⟩\in V\wedge \neg A\in \mathrm{V}\right)\to \left(\neg \exists !y⟨A,y⟩\in V\leftrightarrow \neg \exists !y\varnothing \in V\right)$$
16	12 15	mpbird	$$⊢\left(⟨A,y⟩\in V\wedge \neg A\in \mathrm{V}\right)\to \neg \exists !y⟨A,y⟩\in V$$
17	16	ex	$$⊢⟨A,y⟩\in V\to \left(\neg A\in \mathrm{V}\to \neg \exists !y⟨A,y⟩\in V\right)$$
18	17	con4d	$$⊢⟨A,y⟩\in V\to \left(\exists !y⟨A,y⟩\in V\to A\in \mathrm{V}\right)$$
19	5 18	exlimi	$$⊢\exists y⟨A,y⟩\in V\to \left(\exists !y⟨A,y⟩\in V\to A\in \mathrm{V}\right)$$
20	1 19	mpcom	$$⊢\exists !y⟨A,y⟩\in V\to A\in \mathrm{V}$$