# Metamath Proof Explorer

## Theorem rabun2

Description: Abstraction restricted to a union. (Contributed by Stefan O'Rear, 5-Feb-2015)

Ref Expression
Assertion rabun2 ${⊢}\left\{{x}\in \left({A}\cup {B}\right)|{\phi }\right\}=\left\{{x}\in {A}|{\phi }\right\}\cup \left\{{x}\in {B}|{\phi }\right\}$

### Proof

Step Hyp Ref Expression
1 df-rab ${⊢}\left\{{x}\in \left({A}\cup {B}\right)|{\phi }\right\}=\left\{{x}|\left({x}\in \left({A}\cup {B}\right)\wedge {\phi }\right)\right\}$
2 df-rab ${⊢}\left\{{x}\in {A}|{\phi }\right\}=\left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}$
3 df-rab ${⊢}\left\{{x}\in {B}|{\phi }\right\}=\left\{{x}|\left({x}\in {B}\wedge {\phi }\right)\right\}$
4 2 3 uneq12i ${⊢}\left\{{x}\in {A}|{\phi }\right\}\cup \left\{{x}\in {B}|{\phi }\right\}=\left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}\cup \left\{{x}|\left({x}\in {B}\wedge {\phi }\right)\right\}$
5 elun ${⊢}{x}\in \left({A}\cup {B}\right)↔\left({x}\in {A}\vee {x}\in {B}\right)$
6 5 anbi1i ${⊢}\left({x}\in \left({A}\cup {B}\right)\wedge {\phi }\right)↔\left(\left({x}\in {A}\vee {x}\in {B}\right)\wedge {\phi }\right)$
7 andir ${⊢}\left(\left({x}\in {A}\vee {x}\in {B}\right)\wedge {\phi }\right)↔\left(\left({x}\in {A}\wedge {\phi }\right)\vee \left({x}\in {B}\wedge {\phi }\right)\right)$
8 6 7 bitri ${⊢}\left({x}\in \left({A}\cup {B}\right)\wedge {\phi }\right)↔\left(\left({x}\in {A}\wedge {\phi }\right)\vee \left({x}\in {B}\wedge {\phi }\right)\right)$
9 8 abbii ${⊢}\left\{{x}|\left({x}\in \left({A}\cup {B}\right)\wedge {\phi }\right)\right\}=\left\{{x}|\left(\left({x}\in {A}\wedge {\phi }\right)\vee \left({x}\in {B}\wedge {\phi }\right)\right)\right\}$
10 unab ${⊢}\left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}\cup \left\{{x}|\left({x}\in {B}\wedge {\phi }\right)\right\}=\left\{{x}|\left(\left({x}\in {A}\wedge {\phi }\right)\vee \left({x}\in {B}\wedge {\phi }\right)\right)\right\}$
11 9 10 eqtr4i ${⊢}\left\{{x}|\left({x}\in \left({A}\cup {B}\right)\wedge {\phi }\right)\right\}=\left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}\cup \left\{{x}|\left({x}\in {B}\wedge {\phi }\right)\right\}$
12 4 11 eqtr4i ${⊢}\left\{{x}\in {A}|{\phi }\right\}\cup \left\{{x}\in {B}|{\phi }\right\}=\left\{{x}|\left({x}\in \left({A}\cup {B}\right)\wedge {\phi }\right)\right\}$
13 1 12 eqtr4i ${⊢}\left\{{x}\in \left({A}\cup {B}\right)|{\phi }\right\}=\left\{{x}\in {A}|{\phi }\right\}\cup \left\{{x}\in {B}|{\phi }\right\}$