Theorem exss 1881

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

Assertion

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

Distinct variable group(s):   x,y,A   φ,y

Proof of Theorem exss

Step	Hyp	Ref	Expression
1		df-rab 1208	. . . . 5 ⊢ {x ∈ A∣φ} = {x∣(x ∈ A ∧ φ)}
2	1	cleq1i 1108	. . . 4 ⊢ ({x ∈ A∣φ} = ∅ ↔ {x∣(x ∈ A ∧ φ)} = ∅)
3	2	negbii 162	. . 3 ⊢ (¬ {x ∈ A∣φ} = ∅ ↔ ¬ {x∣(x ∈ A ∧ φ)} = ∅)
4		rabn0 1716	. . 3 ⊢ (¬ {x ∈ A∣φ} = ∅ ↔ ∃x ∈ A φ)
5		n0 1714	. . 3 ⊢ (¬ {x∣(x ∈ A ∧ φ)} = ∅ ↔ ∃z z ∈ {x∣(x ∈ A ∧ φ)})
6	3, 4, 5	3bitr3 156	. 2 ⊢ (∃x ∈ A φ ↔ ∃z z ∈ {x∣(x ∈ A ∧ φ)})
7		snex 1859	. . . . 5 ⊢ {z} ∈ V
8		sseq1 1521	. . . . . 6 ⊢ (y = {z} → (y ⊆ A ↔ {z} ⊆ A))
9		rexeq 1325	. . . . . 6 ⊢ (y = {z} → (∃x ∈ y φ ↔ ∃x ∈ {z}φ))
10	8, 9	anbi12d 476	. . . . 5 ⊢ (y = {z} → ((y ⊆ A ∧ ∃x ∈ y φ) ↔ ({z} ⊆ A ∧ ∃x ∈ {z}φ)))
11	7, 10	cla4ev 1401	. . . 4 ⊢ (({z} ⊆ A ∧ ∃x ∈ {z}φ) → ∃y(y ⊆ A ∧ ∃x ∈ y φ))
12		visset 1350	. . . . . 6 ⊢ z ∈ V
13	12	snss 1849	. . . . 5 ⊢ (z ∈ {x∣(x ∈ A ∧ φ)} ↔ {z} ⊆ {x∣(x ∈ A ∧ φ)})
14		ssab 1555	. . . . . 6 ⊢ {x∣(x ∈ A ∧ φ)} ⊆ A
15		sstr2 1510	. . . . . 6 ⊢ ({z} ⊆ {x∣(x ∈ A ∧ φ)} → ({x∣(x ∈ A ∧ φ)} ⊆ A → {z} ⊆ A))
16	14, 15	mpi 44	. . . . 5 ⊢ ({z} ⊆ {x∣(x ∈ A ∧ φ)} → {z} ⊆ A)
17	13, 16	sylbi 174	. . . 4 ⊢ (z ∈ {x∣(x ∈ A ∧ φ)} → {z} ⊆ A)
18		pm3.27 260	. . . . . . . 8 ⊢ (([z / x]x ∈ A ∧ [z / x]φ) → [z / x]φ)
19		sbeq1 900	. . . . . . . . 9 ⊢ [z / x]x = z
20		elsn 1820	. . . . . . . . . 10 ⊢ (x ∈ {z} ↔ x = z)
21	20	bisb 855	. . . . . . . . 9 ⊢ ([z / x]x ∈ {z} ↔ [z / x]x = z)
22	19, 21	mpbir 165	. . . . . . . 8 ⊢ [z / x]x ∈ {z}
23	18, 22	jctil 240	. . . . . . 7 ⊢ (([z / x]x ∈ A ∧ [z / x]φ) → ([z / x]x ∈ {z} ∧ [z / x]φ))
24		df-clab 1093	. . . . . . . 8 ⊢ (z ∈ {x∣(x ∈ A ∧ φ)} ↔ [z / x](x ∈ A ∧ φ))
25		sban 889	. . . . . . . 8 ⊢ ([z / x](x ∈ A ∧ φ) ↔ ([z / x]x ∈ A ∧ [z / x]φ))
26	24, 25	bitr 151	. . . . . . 7 ⊢ (z ∈ {x∣(x ∈ A ∧ φ)} ↔ ([z / x]x ∈ A ∧ [z / x]φ))
27		df-rab 1208	. . . . . . . . 9 ⊢ {x ∈ {z}∣φ} = {x∣(x ∈ {z} ∧ φ)}
28	27	eleq2i 1153	. . . . . . . 8 ⊢ (z ∈ {x ∈ {z}∣φ} ↔ z ∈ {x∣(x ∈ {z} ∧ φ)})
29		df-clab 1093	. . . . . . . 8 ⊢ (z ∈ {x∣(x ∈ {z} ∧ φ)} ↔ [z / x](x ∈ {z} ∧ φ))
30		sban 889	. . . . . . . 8 ⊢ ([z / x](x ∈ {z} ∧ φ) ↔ ([z / x]x ∈ {z} ∧ [z / x]φ))
31	28, 29, 30	3bitr 155	. . . . . . 7 ⊢ (z ∈ {x ∈ {z}∣φ} ↔ ([z / x]x ∈ {z} ∧ [z / x]φ))
32	23, 26, 31	3imtr4 192	. . . . . 6 ⊢ (z ∈ {x∣(x ∈ A ∧ φ)} → z ∈ {x ∈ {z}∣φ})
33		n0i 1712	. . . . . 6 ⊢ (z ∈ {x ∈ {z}∣φ} → ¬ {x ∈ {z}∣φ} = ∅)
34	32, 33	syl 12	. . . . 5 ⊢ (z ∈ {x∣(x ∈ A ∧ φ)} → ¬ {x ∈ {z}∣φ} = ∅)
35		rabn0 1716	. . . . 5 ⊢ (¬ {x ∈ {z}∣φ} = ∅ ↔ ∃x ∈ {z}φ)
36	34, 35	sylib 173	. . . 4 ⊢ (z ∈ {x∣(x ∈ A ∧ φ)} → ∃x ∈ {z}φ)
37	11, 17, 36	sylanc 361	. . 3 ⊢ (z ∈ {x∣(x ∈ A ∧ φ)} → ∃y(y ⊆ A ∧ ∃x ∈ y φ))
38	37	19.23aiv 952	. 2 ⊢ (∃z z ∈ {x∣(x ∈ A ∧ φ)} → ∃y(y ⊆ A ∧ ∃x ∈ y φ))
39	6, 38	sylbi 174	1 ⊢ (∃x ∈ A φ → ∃y(y ⊆ A ∧ ∃x ∈ y φ))

Syntax hints:  ¬ wn 1   → wi 2   ∧ wa 196  ∃wex 678   = weq 797  [wsb 852  {cab 1090   = wceq 1091   ∈ wcel 1092  ∃wrex 1202  {crab 1204   ⊆ wss 1487  ∅c0 1707  {csn 1808

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-rex 1206  df-rab 1208  df-v 1349  df-dif 1489  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811

metamath.org