prtlem100

		Ref	Expression
	Assertion	prtlem100	$⊢ \exists x \in A (B \in x \land φ) \leftrightarrow \exists x \in (A ∖ \{\emptyset\}) (B \in x \land φ)$

Step	Hyp	Ref	Expression
1		anass	$⊢ ((x \in A \land x \neq \emptyset) \land (B \in x \land φ)) \leftrightarrow (x \in A \land (x \neq \emptyset \land (B \in x \land φ)))$
2		eldifsn	$⊢ x \in (A ∖ \{\emptyset\}) \leftrightarrow (x \in A \land x \neq \emptyset)$
3	2	anbi1i	$⊢ (x \in (A ∖ \{\emptyset\}) \land (B \in x \land φ)) \leftrightarrow ((x \in A \land x \neq \emptyset) \land (B \in x \land φ))$
4		ne0i	$⊢ B \in x \to x \neq \emptyset$
5	4	pm4.71ri	$⊢ B \in x \leftrightarrow (x \neq \emptyset \land B \in x)$
6	5	anbi1i	$⊢ (B \in x \land φ) \leftrightarrow ((x \neq \emptyset \land B \in x) \land φ)$
7		anass	$⊢ ((x \neq \emptyset \land B \in x) \land φ) \leftrightarrow (x \neq \emptyset \land (B \in x \land φ))$
8	6 7	bitri	$⊢ (B \in x \land φ) \leftrightarrow (x \neq \emptyset \land (B \in x \land φ))$
9	8	anbi2i	$⊢ (x \in A \land (B \in x \land φ)) \leftrightarrow (x \in A \land (x \neq \emptyset \land (B \in x \land φ)))$
10	1 3 9	3bitr4ri	$⊢ (x \in A \land (B \in x \land φ)) \leftrightarrow (x \in (A ∖ \{\emptyset\}) \land (B \in x \land φ))$
11	10	rexbii2	$⊢ \exists x \in A (B \in x \land φ) \leftrightarrow \exists x \in (A ∖ \{\emptyset\}) (B \in x \land φ)$

Metamath Proof Explorer