Metamath Proof Explorer


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 syl6bi
 |-  ( -. 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 )