# Metamath Proof Explorer

## Theorem unab

Description: Union of two class abstractions. (Contributed by NM, 29-Sep-2002) (Proof shortened by Andrew Salmon, 26-Jun-2011)

Ref Expression
Assertion unab ${⊢}\left\{{x}|{\phi }\right\}\cup \left\{{x}|{\psi }\right\}=\left\{{x}|\left({\phi }\vee {\psi }\right)\right\}$

### Proof

Step Hyp Ref Expression
1 sbor ${⊢}\left[{y}/{x}\right]\left({\phi }\vee {\psi }\right)↔\left(\left[{y}/{x}\right]{\phi }\vee \left[{y}/{x}\right]{\psi }\right)$
2 df-clab ${⊢}{y}\in \left\{{x}|\left({\phi }\vee {\psi }\right)\right\}↔\left[{y}/{x}\right]\left({\phi }\vee {\psi }\right)$
3 df-clab ${⊢}{y}\in \left\{{x}|{\phi }\right\}↔\left[{y}/{x}\right]{\phi }$
4 df-clab ${⊢}{y}\in \left\{{x}|{\psi }\right\}↔\left[{y}/{x}\right]{\psi }$
5 3 4 orbi12i ${⊢}\left({y}\in \left\{{x}|{\phi }\right\}\vee {y}\in \left\{{x}|{\psi }\right\}\right)↔\left(\left[{y}/{x}\right]{\phi }\vee \left[{y}/{x}\right]{\psi }\right)$
6 1 2 5 3bitr4ri ${⊢}\left({y}\in \left\{{x}|{\phi }\right\}\vee {y}\in \left\{{x}|{\psi }\right\}\right)↔{y}\in \left\{{x}|\left({\phi }\vee {\psi }\right)\right\}$
7 6 uneqri ${⊢}\left\{{x}|{\phi }\right\}\cup \left\{{x}|{\psi }\right\}=\left\{{x}|\left({\phi }\vee {\psi }\right)\right\}$