Theorem exss 2764

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 1649	. . . 4 |- {x e. A | ph} = {x | (x e. A /\ ph)}
2	1	neeq1i 1589	. . 3 |- ({x e. A | ph} =/= (/) <-> {x | (x e. A /\ ph)} =/= (/))
3		rabn0 2288	. . 3 |- ({x e. A | ph} =/= (/) <-> E.x e. A ph)
4		ne0 2284	. . 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 2745	. . . . 5 |- {z} e. V
7		sseq1 2078	. . . . . 6 |- (y = {z} -> (y (_ A <-> {z} (_ A))
8		rexeq1 1784	. . . . . 6 |- (y = {z} -> (E.x e. y ph <-> E.x e. {z}ph))
9	7, 8	anbi12d 627	. . . . 5 |- (y = {z} -> ((y (_ A /\ E.x e. y ph) <-> ({z} (_ A /\ E.x e. {z}ph)))
10	6, 9	cla4ev 1865	. . . 4 |- (({z} (_ A /\ E.x e. {z}ph) -> E.y(y (_ A /\ E.x e. y ph))
11		visset 1809	. . . . . 6 |- z e. V
12	11	snss 2457	. . . . 5 |- (z e. {x | (x e. A /\ ph)} <-> {z} (_ {x | (x e. A /\ ph)})
13		ssab2 2126	. . . . . 6 |- {x | (x e. A /\ ph)} (_ A
14		sstr2 2067	. . . . . 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 1191	. . . . . . . . 9 |- [z / x]x = z
19		elsn 2417	. . . . . . . . . 10 |- (x e. {z} <-> x = z)
20	19	sbbii 1172	. . . . . . . . 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 1462	. . . . . . . 8 |- (z e. {x | (x e. A /\ ph)} <-> [z / x](x e. A /\ ph))
24		sban 1235	. . . . . . . 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 1649	. . . . . . . . 9 |- {x e. {z} | ph} = {x | (x e. {z} /\ ph)}
27	26	eleq2i 1535	. . . . . . . 8 |- (z e. {x e. {z} | ph} <-> z e. {x | (x e. {z} /\ ph)})
28		df-clab 1462	. . . . . . . 8 |- (z e. {x | (x e. {z} /\ ph)} <-> [z / x](x e. {z} /\ ph))
29		sban 1235	. . . . . . . 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 2282	. . . . . 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 2288	. . . . 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 471	. . 3 |- (z e. {x | (x e. A /\ ph)} -> E.y(y (_ A /\ E.x e. y ph))
37	36	19.23aiv 1293	. 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 954   e. wcel 956  E.wex 978  [wsbc 1168  {cab 1461   =/= wne 1582  E.wrex 1643  {crab 1645   (_ wss 2043  (/)c0 2276  {csn 2405

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698  ax-pow 2737

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-rex 1647  df-rab 1649  df-v 1808  df-dif 2045  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408

Copyright terms: Public domain