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	|- ( E! y <. A , y >. e. V -> A e. _V )

Proof

Step	Hyp	Ref	Expression
1		euex	|- ( E! y <. A , y >. e. V -> E. y <. A , y >. e. V )
2		nfeu1	|- F/ y E! y <. A , y >. e. V
3		nfcv	|- F/_ y A
4	3	nfel1	|- F/ y A e. _V
5	2 4	nfim	|- F/ y ( E! y <. A , y >. e. V -> A e. _V )
6		opprc1	|- ( -. A e. _V -> <. A , y >. = (/) )
7	6	eleq1d	|- ( -. A e. _V -> ( <. A , y >. e. V <-> (/) e. V ) )
8		ax-5	|- ( (/) e. V -> A. y (/) e. V )
9		alneu	|- ( A. y (/) e. V -> -. E! y (/) e. V )
10	8 9	syl	|- ( (/) e. V -> -. E! y (/) e. V )
11	7 10	biimtrdi	|- ( -. A e. _V -> ( <. A , y >. e. V -> -. E! y (/) e. V ) )
12	11	impcom	|- ( ( <. A , y >. e. V /\ -. A e. _V ) -> -. E! y (/) e. V )
13	7	eubidv	|- ( -. A e. _V -> ( E! y <. A , y >. e. V <-> E! y (/) e. V ) )
14	13	notbid	|- ( -. A e. _V -> ( -. E! y <. A , y >. e. V <-> -. E! y (/) e. V ) )
15	14	adantl	|- ( ( <. A , y >. e. V /\ -. A e. _V ) -> ( -. E! y <. A , y >. e. V <-> -. E! y (/) e. V ) )
16	12 15	mpbird	|- ( ( <. A , y >. e. V /\ -. A e. _V ) -> -. E! y <. A , y >. e. V )
17	16	ex	|- ( <. A , y >. e. V -> ( -. A e. _V -> -. E! y <. A , y >. e. V ) )
18	17	con4d	|- ( <. A , y >. e. V -> ( E! y <. A , y >. e. V -> A e. _V ) )
19	5 18	exlimi	|- ( E. y <. A , y >. e. V -> ( E! y <. A , y >. e. V -> A e. _V ) )
20	1 19	mpcom	|- ( E! y <. A , y >. e. V -> A e. _V )