# Metamath Proof Explorer

## Theorem undisjrab

Description: Union of two disjoint restricted class abstractions; compare unrab . (Contributed by Steve Rodriguez, 28-Feb-2020)

Ref Expression
Assertion undisjrab ${⊢}\left\{{x}\in {A}|{\phi }\right\}\cap \left\{{x}\in {A}|{\psi }\right\}=\varnothing ↔\left\{{x}\in {A}|{\phi }\right\}\cup \left\{{x}\in {A}|{\psi }\right\}=\left\{{x}\in {A}|\left({\phi }⊻{\psi }\right)\right\}$

### Proof

Step Hyp Ref Expression
1 rabeq0 ${⊢}\left\{{x}\in {A}|\left({\phi }\wedge {\psi }\right)\right\}=\varnothing ↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬\left({\phi }\wedge {\psi }\right)$
2 df-nan ${⊢}\left({\phi }⊼{\psi }\right)↔¬\left({\phi }\wedge {\psi }\right)$
3 nanorxor ${⊢}\left({\phi }⊼{\psi }\right)↔\left(\left({\phi }\vee {\psi }\right)↔\left({\phi }⊻{\psi }\right)\right)$
4 2 3 bitr3i ${⊢}¬\left({\phi }\wedge {\psi }\right)↔\left(\left({\phi }\vee {\psi }\right)↔\left({\phi }⊻{\psi }\right)\right)$
5 4 ralbii ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬\left({\phi }\wedge {\psi }\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\vee {\psi }\right)↔\left({\phi }⊻{\psi }\right)\right)$
6 rabbi ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\vee {\psi }\right)↔\left({\phi }⊻{\psi }\right)\right)↔\left\{{x}\in {A}|\left({\phi }\vee {\psi }\right)\right\}=\left\{{x}\in {A}|\left({\phi }⊻{\psi }\right)\right\}$
7 1 5 6 3bitri ${⊢}\left\{{x}\in {A}|\left({\phi }\wedge {\psi }\right)\right\}=\varnothing ↔\left\{{x}\in {A}|\left({\phi }\vee {\psi }\right)\right\}=\left\{{x}\in {A}|\left({\phi }⊻{\psi }\right)\right\}$
8 inrab ${⊢}\left\{{x}\in {A}|{\phi }\right\}\cap \left\{{x}\in {A}|{\psi }\right\}=\left\{{x}\in {A}|\left({\phi }\wedge {\psi }\right)\right\}$
9 8 eqeq1i ${⊢}\left\{{x}\in {A}|{\phi }\right\}\cap \left\{{x}\in {A}|{\psi }\right\}=\varnothing ↔\left\{{x}\in {A}|\left({\phi }\wedge {\psi }\right)\right\}=\varnothing$
10 unrab ${⊢}\left\{{x}\in {A}|{\phi }\right\}\cup \left\{{x}\in {A}|{\psi }\right\}=\left\{{x}\in {A}|\left({\phi }\vee {\psi }\right)\right\}$
11 10 eqeq1i ${⊢}\left\{{x}\in {A}|{\phi }\right\}\cup \left\{{x}\in {A}|{\psi }\right\}=\left\{{x}\in {A}|\left({\phi }⊻{\psi }\right)\right\}↔\left\{{x}\in {A}|\left({\phi }\vee {\psi }\right)\right\}=\left\{{x}\in {A}|\left({\phi }⊻{\psi }\right)\right\}$
12 7 9 11 3bitr4i ${⊢}\left\{{x}\in {A}|{\phi }\right\}\cap \left\{{x}\in {A}|{\psi }\right\}=\varnothing ↔\left\{{x}\in {A}|{\phi }\right\}\cup \left\{{x}\in {A}|{\psi }\right\}=\left\{{x}\in {A}|\left({\phi }⊻{\psi }\right)\right\}$