unisn2

Description: A version of unisn without the A e. _V hypothesis. (Contributed by Stefan Allan, 14-Mar-2006)

		Ref	Expression
	Assertion	unisn2	$⊢ ⋃ \{A\} \in \{\emptyset, A\}$

Step	Hyp	Ref	Expression
1		unisng	$⊢ A \in V \to ⋃ \{A\} = A$
2		prid2g	$⊢ A \in V \to A \in \{\emptyset, A\}$
3	1 2	eqeltrd	$⊢ A \in V \to ⋃ \{A\} \in \{\emptyset, A\}$
4		snprc	$⊢ \neg A \in V \leftrightarrow \{A\} = \emptyset$
5	4	biimpi	$⊢ \neg A \in V \to \{A\} = \emptyset$
6	5	unieqd	$⊢ \neg A \in V \to ⋃ \{A\} = ⋃ \emptyset$
7		uni0	$⊢ ⋃ \emptyset = \emptyset$
8		0ex	$⊢ \emptyset \in V$
9	8	prid1	$⊢ \emptyset \in \{\emptyset, A\}$
10	7 9	eqeltri	$⊢ ⋃ \emptyset \in \{\emptyset, A\}$
11	6 10	eqeltrdi	$⊢ \neg A \in V \to ⋃ \{A\} \in \{\emptyset, A\}$
12	3 11	pm2.61i	$⊢ ⋃ \{A\} \in \{\emptyset, A\}$

Metamath Proof Explorer