Theorem exss

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

	Ref	Expression
Assertion	exss	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ ∃ 𝑥 ∈ 𝑦 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		df-rab	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) }
2	1	neeq1i	⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ≠ ∅ ↔ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ≠ ∅ )
3		rabn0	⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ≠ ∅ ↔ ∃ 𝑥 ∈ 𝐴 𝜑 )
4		n0	⊢ ( { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } )
5	2 3 4	3bitr3i	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑧 𝑧 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } )
6		vex	⊢ 𝑧 ∈ V
7	6	snss	⊢ ( 𝑧 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ↔ { 𝑧 } ⊆ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } )
8		ssab2	⊢ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ⊆ 𝐴
9		sstr2	⊢ ( { 𝑧 } ⊆ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } → ( { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ⊆ 𝐴 → { 𝑧 } ⊆ 𝐴 ) )
10	8 9	mpi	⊢ ( { 𝑧 } ⊆ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } → { 𝑧 } ⊆ 𝐴 )
11	7 10	sylbi	⊢ ( 𝑧 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } → { 𝑧 } ⊆ 𝐴 )
12		simpr	⊢ ( ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) → [ 𝑧 / 𝑥 ] 𝜑 )
13		equsb1v	⊢ [ 𝑧 / 𝑥 ] 𝑥 = 𝑧
14		velsn	⊢ ( 𝑥 ∈ { 𝑧 } ↔ 𝑥 = 𝑧 )
15	14	sbbii	⊢ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ { 𝑧 } ↔ [ 𝑧 / 𝑥 ] 𝑥 = 𝑧 )
16	13 15	mpbir	⊢ [ 𝑧 / 𝑥 ] 𝑥 ∈ { 𝑧 }
17	12 16	jctil	⊢ ( ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) → ( [ 𝑧 / 𝑥 ] 𝑥 ∈ { 𝑧 } ∧ [ 𝑧 / 𝑥 ] 𝜑 ) )
18		df-clab	⊢ ( 𝑧 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ↔ [ 𝑧 / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
19		sban	⊢ ( [ 𝑧 / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) )
20	18 19	bitri	⊢ ( 𝑧 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ↔ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) )
21		df-rab	⊢ { 𝑥 ∈ { 𝑧 } ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ { 𝑧 } ∧ 𝜑 ) }
22	21	eleq2i	⊢ ( 𝑧 ∈ { 𝑥 ∈ { 𝑧 } ∣ 𝜑 } ↔ 𝑧 ∈ { 𝑥 ∣ ( 𝑥 ∈ { 𝑧 } ∧ 𝜑 ) } )
23		df-clab	⊢ ( 𝑧 ∈ { 𝑥 ∣ ( 𝑥 ∈ { 𝑧 } ∧ 𝜑 ) } ↔ [ 𝑧 / 𝑥 ] ( 𝑥 ∈ { 𝑧 } ∧ 𝜑 ) )
24		sban	⊢ ( [ 𝑧 / 𝑥 ] ( 𝑥 ∈ { 𝑧 } ∧ 𝜑 ) ↔ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ { 𝑧 } ∧ [ 𝑧 / 𝑥 ] 𝜑 ) )
25	22 23 24	3bitri	⊢ ( 𝑧 ∈ { 𝑥 ∈ { 𝑧 } ∣ 𝜑 } ↔ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ { 𝑧 } ∧ [ 𝑧 / 𝑥 ] 𝜑 ) )
26	17 20 25	3imtr4i	⊢ ( 𝑧 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } → 𝑧 ∈ { 𝑥 ∈ { 𝑧 } ∣ 𝜑 } )
27	26	ne0d	⊢ ( 𝑧 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } → { 𝑥 ∈ { 𝑧 } ∣ 𝜑 } ≠ ∅ )
28		rabn0	⊢ ( { 𝑥 ∈ { 𝑧 } ∣ 𝜑 } ≠ ∅ ↔ ∃ 𝑥 ∈ { 𝑧 } 𝜑 )
29	27 28	sylib	⊢ ( 𝑧 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } → ∃ 𝑥 ∈ { 𝑧 } 𝜑 )
30		snex	⊢ { 𝑧 } ∈ V
31		sseq1	⊢ ( 𝑦 = { 𝑧 } → ( 𝑦 ⊆ 𝐴 ↔ { 𝑧 } ⊆ 𝐴 ) )
32		rexeq	⊢ ( 𝑦 = { 𝑧 } → ( ∃ 𝑥 ∈ 𝑦 𝜑 ↔ ∃ 𝑥 ∈ { 𝑧 } 𝜑 ) )
33	31 32	anbi12d	⊢ ( 𝑦 = { 𝑧 } → ( ( 𝑦 ⊆ 𝐴 ∧ ∃ 𝑥 ∈ 𝑦 𝜑 ) ↔ ( { 𝑧 } ⊆ 𝐴 ∧ ∃ 𝑥 ∈ { 𝑧 } 𝜑 ) ) )
34	30 33	spcev	⊢ ( ( { 𝑧 } ⊆ 𝐴 ∧ ∃ 𝑥 ∈ { 𝑧 } 𝜑 ) → ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ ∃ 𝑥 ∈ 𝑦 𝜑 ) )
35	11 29 34	syl2anc	⊢ ( 𝑧 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } → ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ ∃ 𝑥 ∈ 𝑦 𝜑 ) )
36	35	exlimiv	⊢ ( ∃ 𝑧 𝑧 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } → ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ ∃ 𝑥 ∈ 𝑦 𝜑 ) )
37	5 36	sylbi	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ ∃ 𝑥 ∈ 𝑦 𝜑 ) )