unisnif

Description: Express union of singleton in terms of if . (Contributed by Scott Fenton, 27-Mar-2014) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	unisnif	$⊢ ⋃ \{A\} = if (A \in V, A, \emptyset)$

Step	Hyp	Ref	Expression
1		iftrue	$⊢ A \in V \to if (A \in V, A, \emptyset) = A$
2		unisng	$⊢ A \in V \to ⋃ \{A\} = A$
3	1 2	eqtr4d	$⊢ A \in V \to if (A \in V, A, \emptyset) = ⋃ \{A\}$
4		iffalse	$⊢ \neg A \in V \to if (A \in V, A, \emptyset) = \emptyset$
5		snprc	$⊢ \neg A \in V \leftrightarrow \{A\} = \emptyset$
6	5	biimpi	$⊢ \neg A \in V \to \{A\} = \emptyset$
7	6	unieqd	$⊢ \neg A \in V \to ⋃ \{A\} = ⋃ \emptyset$
8		uni0	$⊢ ⋃ \emptyset = \emptyset$
9	7 8	eqtrdi	$⊢ \neg A \in V \to ⋃ \{A\} = \emptyset$
10	4 9	eqtr4d	$⊢ \neg A \in V \to if (A \in V, A, \emptyset) = ⋃ \{A\}$
11	3 10	pm2.61i	$⊢ if (A \in V, A, \emptyset) = ⋃ \{A\}$
12	11	eqcomi	$⊢ ⋃ \{A\} = if (A \in V, A, \emptyset)$

Metamath Proof Explorer