Theorem exss 3933

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

Assertion

Ref	Expression
exss	⊢ (∃x ∈ A φ → ∃y(y ⊆ A ∧ ∃x ∈ y φ))

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

Allowed substitution hint:   φ(x)

Proof of Theorem exss

Dummy variables z w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rabn0m 3218	. . 3 ⊢ (∃z z ∈ {x ∈ A ∣ φ} ↔ ∃x ∈ A φ)
2		df-rab 2289	. . . . 5 ⊢ {x ∈ A ∣ φ} = {x ∣ (x ∈ A ∧ φ)}
3	2	eleq2i 2082	. . . 4 ⊢ (z ∈ {x ∈ A ∣ φ} ↔ z ∈ {x ∣ (x ∈ A ∧ φ)})
4	3	exbii 1474	. . 3 ⊢ (∃z z ∈ {x ∈ A ∣ φ} ↔ ∃z z ∈ {x ∣ (x ∈ A ∧ φ)})
5	1, 4	bitr3i 175	. 2 ⊢ (∃x ∈ A φ ↔ ∃z z ∈ {x ∣ (x ∈ A ∧ φ)})
6		vex 2534	. . . . . 6 ⊢ z ∈ V
7	6	snss 3464	. . . . 5 ⊢ (z ∈ {x ∣ (x ∈ A ∧ φ)} ↔ {z} ⊆ {x ∣ (x ∈ A ∧ φ)})
8		ssab2 2997	. . . . . 6 ⊢ {x ∣ (x ∈ A ∧ φ)} ⊆ A
9		sstr2 2925	. . . . . 6 ⊢ ({z} ⊆ {x ∣ (x ∈ A ∧ φ)} → ({x ∣ (x ∈ A ∧ φ)} ⊆ A → {z} ⊆ A))
10	8, 9	mpi 15	. . . . 5 ⊢ ({z} ⊆ {x ∣ (x ∈ A ∧ φ)} → {z} ⊆ A)
11	7, 10	sylbi 114	. . . 4 ⊢ (z ∈ {x ∣ (x ∈ A ∧ φ)} → {z} ⊆ A)
12		simpr 103	. . . . . . . 8 ⊢ (([z / x]x ∈ A ∧ [z / x]φ) → [z / x]φ)
13		equsb1 1646	. . . . . . . . 9 ⊢ [z / x]x = z
14		elsn 3361	. . . . . . . . . 10 ⊢ (x ∈ {z} ↔ x = z)
15	14	sbbii 1626	. . . . . . . . 9 ⊢ ([z / x]x ∈ {z} ↔ [z / x]x = z)
16	13, 15	mpbir 134	. . . . . . . 8 ⊢ [z / x]x ∈ {z}
17	12, 16	jctil 295	. . . . . . 7 ⊢ (([z / x]x ∈ A ∧ [z / x]φ) → ([z / x]x ∈ {z} ∧ [z / x]φ))
18		df-clab 2005	. . . . . . . 8 ⊢ (z ∈ {x ∣ (x ∈ A ∧ φ)} ↔ [z / x](x ∈ A ∧ φ))
19		sban 1807	. . . . . . . 8 ⊢ ([z / x](x ∈ A ∧ φ) ↔ ([z / x]x ∈ A ∧ [z / x]φ))
20	18, 19	bitri 173	. . . . . . 7 ⊢ (z ∈ {x ∣ (x ∈ A ∧ φ)} ↔ ([z / x]x ∈ A ∧ [z / x]φ))
21		df-rab 2289	. . . . . . . . 9 ⊢ {x ∈ {z} ∣ φ} = {x ∣ (x ∈ {z} ∧ φ)}
22	21	eleq2i 2082	. . . . . . . 8 ⊢ (z ∈ {x ∈ {z} ∣ φ} ↔ z ∈ {x ∣ (x ∈ {z} ∧ φ)})
23		df-clab 2005	. . . . . . . . 9 ⊢ (z ∈ {x ∣ (x ∈ {z} ∧ φ)} ↔ [z / x](x ∈ {z} ∧ φ))
24		sban 1807	. . . . . . . . 9 ⊢ ([z / x](x ∈ {z} ∧ φ) ↔ ([z / x]x ∈ {z} ∧ [z / x]φ))
25	23, 24	bitri 173	. . . . . . . 8 ⊢ (z ∈ {x ∣ (x ∈ {z} ∧ φ)} ↔ ([z / x]x ∈ {z} ∧ [z / x]φ))
26	22, 25	bitri 173	. . . . . . 7 ⊢ (z ∈ {x ∈ {z} ∣ φ} ↔ ([z / x]x ∈ {z} ∧ [z / x]φ))
27	17, 20, 26	3imtr4i 190	. . . . . 6 ⊢ (z ∈ {x ∣ (x ∈ A ∧ φ)} → z ∈ {x ∈ {z} ∣ φ})
28		elex2 2543	. . . . . 6 ⊢ (z ∈ {x ∈ {z} ∣ φ} → ∃w w ∈ {x ∈ {z} ∣ φ})
29	27, 28	syl 14	. . . . 5 ⊢ (z ∈ {x ∣ (x ∈ A ∧ φ)} → ∃w w ∈ {x ∈ {z} ∣ φ})
30		rabn0m 3218	. . . . 5 ⊢ (∃w w ∈ {x ∈ {z} ∣ φ} ↔ ∃x ∈ {z}φ)
31	29, 30	sylib 127	. . . 4 ⊢ (z ∈ {x ∣ (x ∈ A ∧ φ)} → ∃x ∈ {z}φ)
32		snexgOLD 3905	. . . . . 6 ⊢ (z ∈ V → {z} ∈ V)
33	6, 32	ax-mp 7	. . . . 5 ⊢ {z} ∈ V
34		sseq1 2939	. . . . . 6 ⊢ (y = {z} → (y ⊆ A ↔ {z} ⊆ A))
35		rexeq 2480	. . . . . 6 ⊢ (y = {z} → (∃x ∈ y φ ↔ ∃x ∈ {z}φ))
36	34, 35	anbi12d 445	. . . . 5 ⊢ (y = {z} → ((y ⊆ A ∧ ∃x ∈ y φ) ↔ ({z} ⊆ A ∧ ∃x ∈ {z}φ)))
37	33, 36	spcev 2620	. . . 4 ⊢ (({z} ⊆ A ∧ ∃x ∈ {z}φ) → ∃y(y ⊆ A ∧ ∃x ∈ y φ))
38	11, 31, 37	syl2anc 393	. . 3 ⊢ (z ∈ {x ∣ (x ∈ A ∧ φ)} → ∃y(y ⊆ A ∧ ∃x ∈ y φ))
39	38	exlimiv 1467	. 2 ⊢ (∃z z ∈ {x ∣ (x ∈ A ∧ φ)} → ∃y(y ⊆ A ∧ ∃x ∈ y φ))
40	5, 39	sylbi 114	1 ⊢ (∃x ∈ A φ → ∃y(y ⊆ A ∧ ∃x ∈ y φ))

Syntax hints:   → wi 4   ∧ wa 97   = wceq 1226  ∃wex 1358   ∈ wcel 1370  [wsb 1623  {cab 2004  ∃wrex 2281  {crab 2284  Vcvv 2531   ⊆ wss 2890  {csn 3346

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-14 1382  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-sep 3845  ax-pow 3897

This theorem depends on definitions:  df-bi 110  df-tru 1229  df-nf 1326  df-sb 1624  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-rex 2286  df-rab 2289  df-v 2533  df-in 2897  df-ss 2904  df-pw 3332  df-sn 3352

This theorem is referenced by: (None)