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		snex	|- { 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 ) )