This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

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