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	$⊢ \exists x \in A φ \to \exists y (y \subseteq A \land \exists x \in y φ)$

Proof

Step	Hyp	Ref	Expression
1		df-rab	$⊢ \{x \in A \| φ\} = \{x \| (x \in A \land φ)\}$
2	1	neeq1i	$⊢ \{x \in A \| φ\} \neq \emptyset \leftrightarrow \{x \| (x \in A \land φ)\} \neq \emptyset$
3		rabn0	$⊢ \{x \in A \| φ\} \neq \emptyset \leftrightarrow \exists x \in A φ$
4		n0	$⊢ \{x \| (x \in A \land φ)\} \neq \emptyset \leftrightarrow \exists z z \in \{x \| (x \in A \land φ)\}$
5	2 3 4	3bitr3i	$⊢ \exists x \in A φ \leftrightarrow \exists z z \in \{x \| (x \in A \land φ)\}$
6		vex	$⊢ z \in V$
7	6	snss	$⊢ z \in \{x \| (x \in A \land φ)\} \leftrightarrow \{z\} \subseteq \{x \| (x \in A \land φ)\}$
8		ssab2	$⊢ \{x \| (x \in A \land φ)\} \subseteq A$
9		sstr2	$⊢ \{z\} \subseteq \{x \| (x \in A \land φ)\} \to (\{x \| (x \in A \land φ)\} \subseteq A \to \{z\} \subseteq A)$
10	8 9	mpi	$⊢ \{z\} \subseteq \{x \| (x \in A \land φ)\} \to \{z\} \subseteq A$
11	7 10	sylbi	$⊢ z \in \{x \| (x \in A \land φ)\} \to \{z\} \subseteq A$
12		simpr	$⊢ ([z/ x] x \in A \land [z/ x] φ) \to [z/ x] φ$
13		equsb1v	$⊢ [z/ x] x = z$
14		velsn	$⊢ x \in \{z\} \leftrightarrow x = z$
15	14	sbbii	$⊢ [z/ x] x \in \{z\} \leftrightarrow [z/ x] x = z$
16	13 15	mpbir	$⊢ [z/ x] x \in \{z\}$
17	12 16	jctil	$⊢ ([z/ x] x \in A \land [z/ x] φ) \to ([z/ x] x \in \{z\} \land [z/ x] φ)$
18		df-clab	$⊢ z \in \{x \| (x \in A \land φ)\} \leftrightarrow [z/ x] (x \in A \land φ)$
19		sban	$⊢ [z/ x] (x \in A \land φ) \leftrightarrow ([z/ x] x \in A \land [z/ x] φ)$
20	18 19	bitri	$⊢ z \in \{x \| (x \in A \land φ)\} \leftrightarrow ([z/ x] x \in A \land [z/ x] φ)$
21		df-rab	$⊢ \{x \in \{z\} \| φ\} = \{x \| (x \in \{z\} \land φ)\}$
22	21	eleq2i	$⊢ z \in \{x \in \{z\} \| φ\} \leftrightarrow z \in \{x \| (x \in \{z\} \land φ)\}$
23		df-clab	$⊢ z \in \{x \| (x \in \{z\} \land φ)\} \leftrightarrow [z/ x] (x \in \{z\} \land φ)$
24		sban	$⊢ [z/ x] (x \in \{z\} \land φ) \leftrightarrow ([z/ x] x \in \{z\} \land [z/ x] φ)$
25	22 23 24	3bitri	$⊢ z \in \{x \in \{z\} \| φ\} \leftrightarrow ([z/ x] x \in \{z\} \land [z/ x] φ)$
26	17 20 25	3imtr4i	$⊢ z \in \{x \| (x \in A \land φ)\} \to z \in \{x \in \{z\} \| φ\}$
27	26	ne0d	$⊢ z \in \{x \| (x \in A \land φ)\} \to \{x \in \{z\} \| φ\} \neq \emptyset$
28		rabn0	$⊢ \{x \in \{z\} \| φ\} \neq \emptyset \leftrightarrow \exists x \in \{z\} φ$
29	27 28	sylib	$⊢ z \in \{x \| (x \in A \land φ)\} \to \exists x \in \{z\} φ$
30		snex	$⊢ \{z\} \in V$
31		sseq1	$⊢ y = \{z\} \to (y \subseteq A \leftrightarrow \{z\} \subseteq A)$
32		rexeq	$⊢ y = \{z\} \to (\exists x \in y φ \leftrightarrow \exists x \in \{z\} φ)$
33	31 32	anbi12d	$⊢ y = \{z\} \to ((y \subseteq A \land \exists x \in y φ) \leftrightarrow (\{z\} \subseteq A \land \exists x \in \{z\} φ))$
34	30 33	spcev	$⊢ (\{z\} \subseteq A \land \exists x \in \{z\} φ) \to \exists y (y \subseteq A \land \exists x \in y φ)$
35	11 29 34	syl2anc	$⊢ z \in \{x \| (x \in A \land φ)\} \to \exists y (y \subseteq A \land \exists x \in y φ)$
36	35	exlimiv	$⊢ \exists z z \in \{x \| (x \in A \land φ)\} \to \exists y (y \subseteq A \land \exists x \in y φ)$
37	5 36	sylbi	$⊢ \exists x \in A φ \to \exists y (y \subseteq A \land \exists x \in y φ)$

Metamath Proof Explorer

Theorem exss

Proof