Theorem wuntp

Description: A weak universe is closed under unordered triple. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	wununi.1	$$⊢\phi \to U\in \mathrm{WUni}$$
	wununi.2	$$⊢\phi \to A\in U$$
	wunpr.3	$$⊢\phi \to B\in U$$
	wuntp.3	$$⊢\phi \to C\in U$$
Assertion	wuntp	$$⊢\phi \to \left\{A,B,C\right\}\in U$$

Proof

Step	Hyp	Ref	Expression
1		wununi.1	$$⊢\phi \to U\in \mathrm{WUni}$$
2		wununi.2	$$⊢\phi \to A\in U$$
3		wunpr.3	$$⊢\phi \to B\in U$$
4		wuntp.3	$$⊢\phi \to C\in U$$
5		tpass	$$⊢\left\{A,B,C\right\}=\left\{A\right\}\cup \left\{B,C\right\}$$
6		dfsn2	$$⊢\left\{A\right\}=\left\{A,A\right\}$$
7	1 2 2	wunpr	$$⊢\phi \to \left\{A,A\right\}\in U$$
8	6 7	eqeltrid	$$⊢\phi \to \left\{A\right\}\in U$$
9	1 3 4	wunpr	$$⊢\phi \to \left\{B,C\right\}\in U$$
10	1 8 9	wunun	$$⊢\phi \to \left\{A\right\}\cup \left\{B,C\right\}\in U$$
11	5 10	eqeltrid	$$⊢\phi \to \left\{A,B,C\right\}\in U$$