Theorem exss 2775

Description: Restricted existence in a class (even if proper) implies restricted existence in a subset.

Assertion

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

Distinct variable groups:   x,y,A   ph,y

Proof of Theorem exss

Step	Hyp	Ref	Expression
1		df-rab 1655	. . . 4 |- {x e. A | ph} = {x | (x e. A /\ ph)}
2	1	neeq1i 1595	. . 3 |- ({x e. A | ph} =/= (/) <-> {x | (x e. A /\ ph)} =/= (/))
3		rabn0 2296	. . 3 |- ({x e. A | ph} =/= (/) <-> E.x e. A ph)
4		ne0 2292	. . 3 |- ({x | (x e. A /\ ph)} =/= (/) <-> E.z z e. {x | (x e. A /\ ph)})
5	2, 3, 4	3bitr3 181	. 2 |- (E.x e. A ph <-> E.z z e. {x | (x e. A /\ ph)})
6		snex 2756	. . . . 5 |- {z} e. V
7		sseq1 2085	. . . . . 6 |- (y = {z} -> (y (_ A <-> {z} (_ A))
8		rexeq1 1790	. . . . . 6 |- (y = {z} -> (E.x e. y ph <-> E.x e. {z}ph))
9	7, 8	anbi12d 630	. . . . 5 |- (y = {z} -> ((y (_ A /\ E.x e. y ph) <-> ({z} (_ A /\ E.x e. {z}ph)))
10	6, 9	cla4ev 1872	. . . 4 |- (({z} (_ A /\ E.x e. {z}ph) -> E.y(y (_ A /\ E.x e. y ph))
11		visset 1816	. . . . . 6 |- z e. V
12	11	snss 2465	. . . . 5 |- (z e. {x | (x e. A /\ ph)} <-> {z} (_ {x | (x e. A /\ ph)})
13		ssab2 2133	. . . . . 6 |- {x | (x e. A /\ ph)} (_ A
14		sstr2 2074	. . . . . 6 |- ({z} (_ {x | (x e. A /\ ph)} -> ({x | (x e. A /\ ph)} (_ A -> {z} (_ A))
15	13, 14	mpi 44	. . . . 5 |- ({z} (_ {x | (x e. A /\ ph)} -> {z} (_ A)
16	12, 15	sylbi 199	. . . 4 |- (z e. {x | (x e. A /\ ph)} -> {z} (_ A)
17		pm3.27 323	. . . . . . . 8 |- (([z / x]x e. A /\ [z / x]ph) -> [z / x]ph)
18		equsb1 1195	. . . . . . . . 9 |- [z / x]x = z
19		elsn 2425	. . . . . . . . . 10 |- (x e. {z} <-> x = z)
20	19	sbbii 1176	. . . . . . . . 9 |- ([z / x]x e. {z} <-> [z / x]x = z)
21	18, 20	mpbir 190	. . . . . . . 8 |- [z / x]x e. {z}
22	17, 21	jctil 292	. . . . . . 7 |- (([z / x]x e. A /\ [z / x]ph) -> ([z / x]x e. {z} /\ [z / x]ph))
23		df-clab 1467	. . . . . . . 8 |- (z e. {x | (x e. A /\ ph)} <-> [z / x](x e. A /\ ph))
24		sban 1239	. . . . . . . 8 |- ([z / x](x e. A /\ ph) <-> ([z / x]x e. A /\ [z / x]ph))
25	23, 24	bitr 173	. . . . . . 7 |- (z e. {x | (x e. A /\ ph)} <-> ([z / x]x e. A /\ [z / x]ph))
26		df-rab 1655	. . . . . . . . 9 |- {x e. {z} | ph} = {x | (x e. {z} /\ ph)}
27	26	eleq2i 1541	. . . . . . . 8 |- (z e. {x e. {z} | ph} <-> z e. {x | (x e. {z} /\ ph)})
28		df-clab 1467	. . . . . . . 8 |- (z e. {x | (x e. {z} /\ ph)} <-> [z / x](x e. {z} /\ ph))
29		sban 1239	. . . . . . . 8 |- ([z / x](x e. {z} /\ ph) <-> ([z / x]x e. {z} /\ [z / x]ph))
30	27, 28, 29	3bitr 177	. . . . . . 7 |- (z e. {x e. {z} | ph} <-> ([z / x]x e. {z} /\ [z / x]ph))
31	22, 25, 30	3imtr4 219	. . . . . 6 |- (z e. {x | (x e. A /\ ph)} -> z e. {x e. {z} | ph})
32		ne0i 2289	. . . . . 6 |- (z e. {x e. {z} | ph} -> {x e. {z} | ph} =/= (/))
33	31, 32	syl 10	. . . . 5 |- (z e. {x | (x e. A /\ ph)} -> {x e. {z} | ph} =/= (/))
34		rabn0 2296	. . . . 5 |- ({x e. {z} | ph} =/= (/) <-> E.x e. {z}ph)
35	33, 34	sylib 198	. . . 4 |- (z e. {x | (x e. A /\ ph)} -> E.x e. {z}ph)
36	10, 16, 35	sylanc 473	. . 3 |- (z e. {x | (x e. A /\ ph)} -> E.y(y (_ A /\ E.x e. y ph))
37	36	19.23aiv 1297	. 2 |- (E.z z e. {x | (x e. A /\ ph)} -> E.y(y (_ A /\ E.x e. y ph))
38	5, 37	sylbi 199	1 |- (E.x e. A ph -> E.y(y (_ A /\ E.x e. y ph))

Syntax hints:   -> wi 3   /\ wa 223   = wceq 958   e. wcel 960  E.wex 982  [wsbc 1172  {cab 1466   =/= wne 1588  E.wrex 1649  {crab 1651   (_ wss 2050  (/)c0 2283  {csn 2413

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-sep 2708  ax-pow 2748

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-rex 1653  df-rab 1655  df-v 1815  df-dif 2052  df-in 2054  df-ss 2056  df-nul 2284  df-pw 2406  df-sn 2416

Copyright terms: Public domain