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	⊢ ( ∀ 𝑥 ∈ ∪ 𝐴 ¬ 𝑥 ∈ 𝑥 ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝑦 ¬ 𝑥 ∈ 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		r19.23v	⊢ ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 → ¬ 𝑥 ∈ 𝑥 ) ↔ ( ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 → ¬ 𝑥 ∈ 𝑥 ) )
2	1	albii	⊢ ( ∀ 𝑥 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 → ¬ 𝑥 ∈ 𝑥 ) ↔ ∀ 𝑥 ( ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 → ¬ 𝑥 ∈ 𝑥 ) )
3		ralcom4	⊢ ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ¬ 𝑥 ∈ 𝑥 ) ↔ ∀ 𝑥 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 → ¬ 𝑥 ∈ 𝑥 ) )
4		eluni2	⊢ ( 𝑥 ∈ ∪ 𝐴 ↔ ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 )
5	4	imbi1i	⊢ ( ( 𝑥 ∈ ∪ 𝐴 → ¬ 𝑥 ∈ 𝑥 ) ↔ ( ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 → ¬ 𝑥 ∈ 𝑥 ) )
6	5	albii	⊢ ( ∀ 𝑥 ( 𝑥 ∈ ∪ 𝐴 → ¬ 𝑥 ∈ 𝑥 ) ↔ ∀ 𝑥 ( ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 → ¬ 𝑥 ∈ 𝑥 ) )
7	2 3 6	3bitr4ri	⊢ ( ∀ 𝑥 ( 𝑥 ∈ ∪ 𝐴 → ¬ 𝑥 ∈ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ¬ 𝑥 ∈ 𝑥 ) )
8		df-ral	⊢ ( ∀ 𝑥 ∈ ∪ 𝐴 ¬ 𝑥 ∈ 𝑥 ↔ ∀ 𝑥 ( 𝑥 ∈ ∪ 𝐴 → ¬ 𝑥 ∈ 𝑥 ) )
9		df-ral	⊢ ( ∀ 𝑥 ∈ 𝑦 ¬ 𝑥 ∈ 𝑥 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ¬ 𝑥 ∈ 𝑥 ) )
10	9	ralbii	⊢ ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝑦 ¬ 𝑥 ∈ 𝑥 ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ¬ 𝑥 ∈ 𝑥 ) )
11	7 8 10	3bitr4i	⊢ ( ∀ 𝑥 ∈ ∪ 𝐴 ¬ 𝑥 ∈ 𝑥 ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝑦 ¬ 𝑥 ∈ 𝑥 )