# Metamath Proof Explorer

## Theorem untuni

Description: The union of a class is untangled iff all its members are untangled. (Contributed by Scott Fenton, 28-Feb-2011)

Ref Expression
Assertion untuni ${⊢}\forall {x}\in \bigcup {A}\phantom{\rule{.4em}{0ex}}¬{x}\in {x}↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\forall {x}\in {y}\phantom{\rule{.4em}{0ex}}¬{x}\in {x}$

### Proof

Step Hyp Ref Expression
1 r19.23v ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\to ¬{x}\in {x}\right)↔\left(\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\in {y}\to ¬{x}\in {x}\right)$
2 1 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\to ¬{x}\in {x}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\in {y}\to ¬{x}\in {x}\right)$
3 ralcom4 ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\to ¬{x}\in {x}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\to ¬{x}\in {x}\right)$
4 eluni2 ${⊢}{x}\in \bigcup {A}↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\in {y}$
5 4 imbi1i ${⊢}\left({x}\in \bigcup {A}\to ¬{x}\in {x}\right)↔\left(\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\in {y}\to ¬{x}\in {x}\right)$
6 5 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \bigcup {A}\to ¬{x}\in {x}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\in {y}\to ¬{x}\in {x}\right)$
7 2 3 6 3bitr4ri ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \bigcup {A}\to ¬{x}\in {x}\right)↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\to ¬{x}\in {x}\right)$
8 df-ral ${⊢}\forall {x}\in \bigcup {A}\phantom{\rule{.4em}{0ex}}¬{x}\in {x}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \bigcup {A}\to ¬{x}\in {x}\right)$
9 df-ral ${⊢}\forall {x}\in {y}\phantom{\rule{.4em}{0ex}}¬{x}\in {x}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\to ¬{x}\in {x}\right)$
10 9 ralbii ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\forall {x}\in {y}\phantom{\rule{.4em}{0ex}}¬{x}\in {x}↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\to ¬{x}\in {x}\right)$
11 7 8 10 3bitr4i ${⊢}\forall {x}\in \bigcup {A}\phantom{\rule{.4em}{0ex}}¬{x}\in {x}↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\forall {x}\in {y}\phantom{\rule{.4em}{0ex}}¬{x}\in {x}$