Theorem uniprg

Description: The union of a pair is the union of its members. Proposition 5.7 of TakeutiZaring p. 16. (Contributed by NM, 25-Aug-2006)

	Ref	Expression
Assertion	uniprg	$$⊢\left(A\in V\wedge B\in W\right)\to \bigcup \left\{A,B\right\}=A\cup B$$

Proof

Step	Hyp	Ref	Expression
1		preq1	$$⊢x=A\to \left\{x,y\right\}=\left\{A,y\right\}$$
2	1	unieqd	$$⊢x=A\to \bigcup \left\{x,y\right\}=\bigcup \left\{A,y\right\}$$
3		uneq1	$$⊢x=A\to x\cup y=A\cup y$$
4	2 3	eqeq12d	$$⊢x=A\to \left(\bigcup \left\{x,y\right\}=x\cup y\leftrightarrow \bigcup \left\{A,y\right\}=A\cup y\right)$$
5		preq2	$$⊢y=B\to \left\{A,y\right\}=\left\{A,B\right\}$$
6	5	unieqd	$$⊢y=B\to \bigcup \left\{A,y\right\}=\bigcup \left\{A,B\right\}$$
7		uneq2	$$⊢y=B\to A\cup y=A\cup B$$
8	6 7	eqeq12d	$$⊢y=B\to \left(\bigcup \left\{A,y\right\}=A\cup y\leftrightarrow \bigcup \left\{A,B\right\}=A\cup B\right)$$
9		vex	$$⊢x\in \mathrm{V}$$
10		vex	$$⊢y\in \mathrm{V}$$
11	9 10	unipr	$$⊢\bigcup \left\{x,y\right\}=x\cup y$$
12	4 8 11	vtocl2g	$$⊢\left(A\in V\wedge B\in W\right)\to \bigcup \left\{A,B\right\}=A\cup B$$