# Metamath Proof Explorer

## 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}↔\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}↔\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}$