Theorem uniop

Description: The union of an ordered pair. Theorem 65 of Suppes p. 39. (Contributed by NM, 17-Aug-2004) (Revised by Mario Carneiro, 26-Apr-2015)

	Ref	Expression
Hypotheses	opthw.1	$$⊢A\in \mathrm{V}$$
	opthw.2	$$⊢B\in \mathrm{V}$$
Assertion	uniop	$$⊢\bigcup ⟨A,B⟩=\left\{A,B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		opthw.1	$$⊢A\in \mathrm{V}$$
2		opthw.2	$$⊢B\in \mathrm{V}$$
3	1 2	dfop	$$⊢⟨A,B⟩=\left\{\left\{A\right\},\left\{A,B\right\}\right\}$$
4	3	unieqi	$$⊢\bigcup ⟨A,B⟩=\bigcup \left\{\left\{A\right\},\left\{A,B\right\}\right\}$$
5		snex	$$⊢\left\{A\right\}\in \mathrm{V}$$
6		prex	$$⊢\left\{A,B\right\}\in \mathrm{V}$$
7	5 6	unipr	$$⊢\bigcup \left\{\left\{A\right\},\left\{A,B\right\}\right\}=\left\{A\right\}\cup \left\{A,B\right\}$$
8		snsspr1	$$⊢\left\{A\right\}\subseteq \left\{A,B\right\}$$
9		ssequn1	$$⊢\left\{A\right\}\subseteq \left\{A,B\right\}\leftrightarrow \left\{A\right\}\cup \left\{A,B\right\}=\left\{A,B\right\}$$
10	8 9	mpbi	$$⊢\left\{A\right\}\cup \left\{A,B\right\}=\left\{A,B\right\}$$
11	4 7 10	3eqtri	$$⊢\bigcup ⟨A,B⟩=\left\{A,B\right\}$$