# Metamath Proof Explorer

## Theorem unipr

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

Ref Expression
Hypotheses unipr.1 ${⊢}{A}\in \mathrm{V}$
unipr.2 ${⊢}{B}\in \mathrm{V}$
Assertion unipr ${⊢}\bigcup \left\{{A},{B}\right\}={A}\cup {B}$

### Proof

Step Hyp Ref Expression
1 unipr.1 ${⊢}{A}\in \mathrm{V}$
2 unipr.2 ${⊢}{B}\in \mathrm{V}$
3 19.43 ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {y}\wedge {y}={A}\right)\vee \left({x}\in {y}\wedge {y}={B}\right)\right)↔\left(\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}={A}\right)\vee \exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}={B}\right)\right)$
4 vex ${⊢}{y}\in \mathrm{V}$
5 4 elpr ${⊢}{y}\in \left\{{A},{B}\right\}↔\left({y}={A}\vee {y}={B}\right)$
6 5 anbi2i ${⊢}\left({x}\in {y}\wedge {y}\in \left\{{A},{B}\right\}\right)↔\left({x}\in {y}\wedge \left({y}={A}\vee {y}={B}\right)\right)$
7 andi ${⊢}\left({x}\in {y}\wedge \left({y}={A}\vee {y}={B}\right)\right)↔\left(\left({x}\in {y}\wedge {y}={A}\right)\vee \left({x}\in {y}\wedge {y}={B}\right)\right)$
8 6 7 bitri ${⊢}\left({x}\in {y}\wedge {y}\in \left\{{A},{B}\right\}\right)↔\left(\left({x}\in {y}\wedge {y}={A}\right)\vee \left({x}\in {y}\wedge {y}={B}\right)\right)$
9 8 exbii ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\in \left\{{A},{B}\right\}\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {y}\wedge {y}={A}\right)\vee \left({x}\in {y}\wedge {y}={B}\right)\right)$
10 1 clel3 ${⊢}{x}\in {A}↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}={A}\wedge {x}\in {y}\right)$
11 exancom ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}={A}\wedge {x}\in {y}\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}={A}\right)$
12 10 11 bitri ${⊢}{x}\in {A}↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}={A}\right)$
13 2 clel3 ${⊢}{x}\in {B}↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}={B}\wedge {x}\in {y}\right)$
14 exancom ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}={B}\wedge {x}\in {y}\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}={B}\right)$
15 13 14 bitri ${⊢}{x}\in {B}↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}={B}\right)$
16 12 15 orbi12i ${⊢}\left({x}\in {A}\vee {x}\in {B}\right)↔\left(\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}={A}\right)\vee \exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}={B}\right)\right)$
17 3 9 16 3bitr4ri ${⊢}\left({x}\in {A}\vee {x}\in {B}\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\in \left\{{A},{B}\right\}\right)$
18 17 abbii ${⊢}\left\{{x}|\left({x}\in {A}\vee {x}\in {B}\right)\right\}=\left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\in \left\{{A},{B}\right\}\right)\right\}$
19 df-un ${⊢}{A}\cup {B}=\left\{{x}|\left({x}\in {A}\vee {x}\in {B}\right)\right\}$
20 df-uni ${⊢}\bigcup \left\{{A},{B}\right\}=\left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\in \left\{{A},{B}\right\}\right)\right\}$
21 18 19 20 3eqtr4ri ${⊢}\bigcup \left\{{A},{B}\right\}={A}\cup {B}$