onfrALTlem1

Description: Lemma for onfrALT . (Contributed by Alan Sare, 22-Jul-2012) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	onfrALTlem1	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land a \cap x = \emptyset) \to \exists y \in a a \cap y = \emptyset)$

Step	Hyp	Ref	Expression
1		19.8a	$⊢ (x \in a \land a \cap x = \emptyset) \to \exists x (x \in a \land a \cap x = \emptyset)$
2	1	a1i	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land a \cap x = \emptyset) \to \exists x (x \in a \land a \cap x = \emptyset))$
3		cbvexsv	$⊢ \exists x (x \in a \land a \cap x = \emptyset) \leftrightarrow \exists y [y/ x] (x \in a \land a \cap x = \emptyset)$
4	2 3	syl6ib	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land a \cap x = \emptyset) \to \exists y [y/ x] (x \in a \land a \cap x = \emptyset))$
5		sbsbc	$⊢ [y/ x] (x \in a \land a \cap x = \emptyset) \leftrightarrow \underset{˙}{[} y / x \underset{˙}{]} (x \in a \land a \cap x = \emptyset)$
6		onfrALTlem4	$⊢ \underset{˙}{[} y / x \underset{˙}{]} (x \in a \land a \cap x = \emptyset) \leftrightarrow (y \in a \land a \cap y = \emptyset)$
7	5 6	bitri	$⊢ [y/ x] (x \in a \land a \cap x = \emptyset) \leftrightarrow (y \in a \land a \cap y = \emptyset)$
8	7	exbii	$⊢ \exists y [y/ x] (x \in a \land a \cap x = \emptyset) \leftrightarrow \exists y (y \in a \land a \cap y = \emptyset)$
9	4 8	syl6ib	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land a \cap x = \emptyset) \to \exists y (y \in a \land a \cap y = \emptyset))$
10		df-rex	$⊢ \exists y \in a a \cap y = \emptyset \leftrightarrow \exists y (y \in a \land a \cap y = \emptyset)$
11	9 10	syl6ibr	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land a \cap x = \emptyset) \to \exists y \in a a \cap y = \emptyset)$

Metamath Proof Explorer