This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem exss

Description: Restricted existence in a class (even if proper) implies restricted existence in a subset. (Contributed by NM, 23-Aug-2003)

Ref Expression
Assertion exss 
|- ( E. x e. A ph -> E. y ( y C_ A /\ E. x e. y ph ) )

Proof

Step Hyp Ref Expression
1 df-rab 
 |-  { x e. A | ph } = { x | ( x e. A /\ ph ) }
2 1 neeq1i 
 |-  ( { x e. A | ph } =/= (/) <-> { x | ( x e. A /\ ph ) } =/= (/) )
3 rabn0 
 |-  ( { x e. A | ph } =/= (/) <-> E. x e. A ph )
4 n0 
 |-  ( { x | ( x e. A /\ ph ) } =/= (/) <-> E. z z e. { x | ( x e. A /\ ph ) } )
5 2 3 4 3bitr3i 
 |-  ( E. x e. A ph <-> E. z z e. { x | ( x e. A /\ ph ) } )
6 vex 
 |-  z e. _V
7 6 snss 
 |-  ( z e. { x | ( x e. A /\ ph ) } <-> { z } C_ { x | ( x e. A /\ ph ) } )
8 ssab2 
 |-  { x | ( x e. A /\ ph ) } C_ A
9 sstr2 
 |-  ( { z } C_ { x | ( x e. A /\ ph ) } -> ( { x | ( x e. A /\ ph ) } C_ A -> { z } C_ A ) )
10 8 9 mpi 
 |-  ( { z } C_ { x | ( x e. A /\ ph ) } -> { z } C_ A )
11 7 10 sylbi 
 |-  ( z e. { x | ( x e. A /\ ph ) } -> { z } C_ A )
12 simpr 
 |-  ( ( [ z / x ] x e. A /\ [ z / x ] ph ) -> [ z / x ] ph )
13 equsb1v 
 |-  [ z / x ] x = z
14 velsn 
 |-  ( x e. { z } <-> x = z )
15 14 sbbii 
 |-  ( [ z / x ] x e. { z } <-> [ z / x ] x = z )
16 13 15 mpbir 
 |-  [ z / x ] x e. { z }
17 12 16 jctil 
 |-  ( ( [ z / x ] x e. A /\ [ z / x ] ph ) -> ( [ z / x ] x e. { z } /\ [ z / x ] ph ) )
18 df-clab 
 |-  ( z e. { x | ( x e. A /\ ph ) } <-> [ z / x ] ( x e. A /\ ph ) )
19 sban 
 |-  ( [ z / x ] ( x e. A /\ ph ) <-> ( [ z / x ] x e. A /\ [ z / x ] ph ) )
20 18 19 bitri 
 |-  ( z e. { x | ( x e. A /\ ph ) } <-> ( [ z / x ] x e. A /\ [ z / x ] ph ) )
21 df-rab 
 |-  { x e. { z } | ph } = { x | ( x e. { z } /\ ph ) }
22 21 eleq2i 
 |-  ( z e. { x e. { z } | ph } <-> z e. { x | ( x e. { z } /\ ph ) } )
23 df-clab 
 |-  ( z e. { x | ( x e. { z } /\ ph ) } <-> [ z / x ] ( x e. { z } /\ ph ) )
24 sban 
 |-  ( [ z / x ] ( x e. { z } /\ ph ) <-> ( [ z / x ] x e. { z } /\ [ z / x ] ph ) )
25 22 23 24 3bitri 
 |-  ( z e. { x e. { z } | ph } <-> ( [ z / x ] x e. { z } /\ [ z / x ] ph ) )
26 17 20 25 3imtr4i 
 |-  ( z e. { x | ( x e. A /\ ph ) } -> z e. { x e. { z } | ph } )
27 26 ne0d 
 |-  ( z e. { x | ( x e. A /\ ph ) } -> { x e. { z } | ph } =/= (/) )
28 rabn0 
 |-  ( { x e. { z } | ph } =/= (/) <-> E. x e. { z } ph )
29 27 28 sylib 
 |-  ( z e. { x | ( x e. A /\ ph ) } -> E. x e. { z } ph )
30 vsnex 
 |-  { z } e. _V
31 sseq1 
 |-  ( y = { z } -> ( y C_ A <-> { z } C_ A ) )
32 rexeq 
 |-  ( y = { z } -> ( E. x e. y ph <-> E. x e. { z } ph ) )
33 31 32 anbi12d 
 |-  ( y = { z } -> ( ( y C_ A /\ E. x e. y ph ) <-> ( { z } C_ A /\ E. x e. { z } ph ) ) )
34 30 33 spcev 
 |-  ( ( { z } C_ A /\ E. x e. { z } ph ) -> E. y ( y C_ A /\ E. x e. y ph ) )
35 11 29 34 syl2anc 
 |-  ( z e. { x | ( x e. A /\ ph ) } -> E. y ( y C_ A /\ E. x e. y ph ) )
36 35 exlimiv 
 |-  ( E. z z e. { x | ( x e. A /\ ph ) } -> E. y ( y C_ A /\ E. x e. y ph ) )
37 5 36 sylbi 
 |-  ( E. x e. A ph -> E. y ( y C_ A /\ E. x e. y ph ) )