Theorem exss 3954

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 3239	. . 3 ⊢ (∃z z ∈ {x ∈ A ∣ φ} ↔ ∃x ∈ A φ)
2		df-rab 2309	. . . . 5 ⊢ {x ∈ A ∣ φ} = {x ∣ (x ∈ A ∧ φ)}
3	2	eleq2i 2101	. . . 4 ⊢ (z ∈ {x ∈ A ∣ φ} ↔ z ∈ {x ∣ (x ∈ A ∧ φ)})
4	3	exbii 1493	. . 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 2554	. . . . . 6 ⊢ z ∈ V
7	6	snss 3485	. . . . 5 ⊢ (z ∈ {x ∣ (x ∈ A ∧ φ)} ↔ {z} ⊆ {x ∣ (x ∈ A ∧ φ)})
8		ssab2 3018	. . . . . 6 ⊢ {x ∣ (x ∈ A ∧ φ)} ⊆ A
9		sstr2 2946	. . . . . 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 1665	. . . . . . . . 9 ⊢ [z / x]x = z
14		elsn 3382	. . . . . . . . . 10 ⊢ (x ∈ {z} ↔ x = z)
15	14	sbbii 1645	. . . . . . . . 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 2024	. . . . . . . 8 ⊢ (z ∈ {x ∣ (x ∈ A ∧ φ)} ↔ [z / x](x ∈ A ∧ φ))
19		sban 1826	. . . . . . . 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 2309	. . . . . . . . 9 ⊢ {x ∈ {z} ∣ φ} = {x ∣ (x ∈ {z} ∧ φ)}
22	21	eleq2i 2101	. . . . . . . 8 ⊢ (z ∈ {x ∈ {z} ∣ φ} ↔ z ∈ {x ∣ (x ∈ {z} ∧ φ)})
23		df-clab 2024	. . . . . . . . 9 ⊢ (z ∈ {x ∣ (x ∈ {z} ∧ φ)} ↔ [z / x](x ∈ {z} ∧ φ))
24		sban 1826	. . . . . . . . 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 2564	. . . . . 6 ⊢ (z ∈ {x ∈ {z} ∣ φ} → ∃w w ∈ {x ∈ {z} ∣ φ})
29	27, 28	syl 14	. . . . 5 ⊢ (z ∈ {x ∣ (x ∈ A ∧ φ)} → ∃w w ∈ {x ∈ {z} ∣ φ})
30		rabn0m 3239	. . . . 5 ⊢ (∃w w ∈ {x ∈ {z} ∣ φ} ↔ ∃x ∈ {z}φ)
31	29, 30	sylib 127	. . . 4 ⊢ (z ∈ {x ∣ (x ∈ A ∧ φ)} → ∃x ∈ {z}φ)
32		snexgOLD 3926	. . . . . 6 ⊢ (z ∈ V → {z} ∈ V)
33	6, 32	ax-mp 7	. . . . 5 ⊢ {z} ∈ V
34		sseq1 2960	. . . . . 6 ⊢ (y = {z} → (y ⊆ A ↔ {z} ⊆ A))
35		rexeq 2500	. . . . . 6 ⊢ (y = {z} → (∃x ∈ y φ ↔ ∃x ∈ {z}φ))
36	34, 35	anbi12d 442	. . . . 5 ⊢ (y = {z} → ((y ⊆ A ∧ ∃x ∈ y φ) ↔ ({z} ⊆ A ∧ ∃x ∈ {z}φ)))
37	33, 36	spcev 2641	. . . 4 ⊢ (({z} ⊆ A ∧ ∃x ∈ {z}φ) → ∃y(y ⊆ A ∧ ∃x ∈ y φ))
38	11, 31, 37	syl2anc 391	. . 3 ⊢ (z ∈ {x ∣ (x ∈ A ∧ φ)} → ∃y(y ⊆ A ∧ ∃x ∈ y φ))
39	38	exlimiv 1486	. 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 1242  ∃wex 1378   ∈ wcel 1390  [wsb 1642  {cab 2023  ∃wrex 2301  {crab 2304  Vcvv 2551   ⊆ wss 2911  {csn 3367

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 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918

This theorem depends on definitions:  df-bi 110  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-rex 2306  df-rab 2309  df-v 2553  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373

This theorem is referenced by: (None)