prprrab

Description: The set of proper pairs of elements of a given set expressed in two ways. (Contributed by AV, 24-Nov-2020)

		Ref	Expression
	Assertion	prprrab	$⊢ \{x \in (𝒫 A ∖ \{\emptyset\}) \| \|x\| = 2\} = \{x \in 𝒫 A \| \|x\| = 2\}$

Step	Hyp	Ref	Expression
1		2ne0	$⊢ 2 \neq 0$
2	1	neii	$⊢ \neg 2 = 0$
3		eqeq1	$⊢ \|x\| = 2 \to (\|x\| = 0 \leftrightarrow 2 = 0)$
4	2 3	mtbiri	$⊢ \|x\| = 2 \to \neg \|x\| = 0$
5		hasheq0	$⊢ x \in V \to (\|x\| = 0 \leftrightarrow x = \emptyset)$
6	5	bicomd	$⊢ x \in V \to (x = \emptyset \leftrightarrow \|x\| = 0)$
7	6	necon3abid	$⊢ x \in V \to (x \neq \emptyset \leftrightarrow \neg \|x\| = 0)$
8	7	elv	$⊢ x \neq \emptyset \leftrightarrow \neg \|x\| = 0$
9	4 8	sylibr	$⊢ \|x\| = 2 \to x \neq \emptyset$
10	9	biantrud	$⊢ \|x\| = 2 \to (x \in 𝒫 A \leftrightarrow (x \in 𝒫 A \land x \neq \emptyset))$
11		eldifsn	$⊢ x \in (𝒫 A ∖ \{\emptyset\}) \leftrightarrow (x \in 𝒫 A \land x \neq \emptyset)$
12	10 11	bitr4di	$⊢ \|x\| = 2 \to (x \in 𝒫 A \leftrightarrow x \in (𝒫 A ∖ \{\emptyset\}))$
13	12	pm5.32ri	$⊢ (x \in 𝒫 A \land \|x\| = 2) \leftrightarrow (x \in (𝒫 A ∖ \{\emptyset\}) \land \|x\| = 2)$
14	13	abbii	$⊢ \{x \| (x \in 𝒫 A \land \|x\| = 2)\} = \{x \| (x \in (𝒫 A ∖ \{\emptyset\}) \land \|x\| = 2)\}$
15		df-rab	$⊢ \{x \in 𝒫 A \| \|x\| = 2\} = \{x \| (x \in 𝒫 A \land \|x\| = 2)\}$
16		df-rab	$⊢ \{x \in (𝒫 A ∖ \{\emptyset\}) \| \|x\| = 2\} = \{x \| (x \in (𝒫 A ∖ \{\emptyset\}) \land \|x\| = 2)\}$
17	14 15 16	3eqtr4ri	$⊢ \{x \in (𝒫 A ∖ \{\emptyset\}) \| \|x\| = 2\} = \{x \in 𝒫 A \| \|x\| = 2\}$

Metamath Proof Explorer