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 ⊢ ∀ x ∈ ⋃ A ¬ x ∈ x ↔ ∀ y ∈ A ∀ x ∈ y ¬ x ∈ x

Proof

Step Hyp Ref Expression
1 r19.23v ⊢ ∀ y ∈ A x ∈ y → ¬ x ∈ x ↔ ∃ y ∈ A x ∈ y → ¬ x ∈ x
2 1 albii ⊢ ∀ x ∀ y ∈ A x ∈ y → ¬ x ∈ x ↔ ∀ x ∃ y ∈ A x ∈ y → ¬ x ∈ x
3 ralcom4 ⊢ ∀ y ∈ A ∀ x x ∈ y → ¬ x ∈ x ↔ ∀ x ∀ y ∈ A x ∈ y → ¬ x ∈ x
4 eluni2 ⊢ x ∈ ⋃ A ↔ ∃ y ∈ A x ∈ y
5 4 imbi1i ⊢ x ∈ ⋃ A → ¬ x ∈ x ↔ ∃ y ∈ A x ∈ y → ¬ x ∈ x
6 5 albii ⊢ ∀ x x ∈ ⋃ A → ¬ x ∈ x ↔ ∀ x ∃ y ∈ A x ∈ y → ¬ x ∈ x
7 2 3 6 3bitr4ri ⊢ ∀ x x ∈ ⋃ A → ¬ x ∈ x ↔ ∀ y ∈ A ∀ x x ∈ y → ¬ x ∈ x
8 df-ral ⊢ ∀ x ∈ ⋃ A ¬ x ∈ x ↔ ∀ x x ∈ ⋃ A → ¬ x ∈ x
9 df-ral ⊢ ∀ x ∈ y ¬ x ∈ x ↔ ∀ x x ∈ y → ¬ x ∈ x
10 9 ralbii ⊢ ∀ y ∈ A ∀ x ∈ y ¬ x ∈ x ↔ ∀ y ∈ A ∀ x x ∈ y → ¬ x ∈ x
11 7 8 10 3bitr4i ⊢ ∀ x ∈ ⋃ A ¬ x ∈ x ↔ ∀ y ∈ A ∀ x ∈ y ¬ x ∈ x