Metamath Proof Explorer


Theorem untint

Description: If there is an untangled element of a class, then the intersection of the class is untangled. (Contributed by Scott Fenton, 1-Mar-2011)

Ref Expression
Assertion untint ( ∃ 𝑥𝐴𝑦𝑥 ¬ 𝑦𝑦 → ∀ 𝑦 𝐴 ¬ 𝑦𝑦 )

Proof

Step Hyp Ref Expression
1 intss1 ( 𝑥𝐴 𝐴𝑥 )
2 ssralv ( 𝐴𝑥 → ( ∀ 𝑦𝑥 ¬ 𝑦𝑦 → ∀ 𝑦 𝐴 ¬ 𝑦𝑦 ) )
3 1 2 syl ( 𝑥𝐴 → ( ∀ 𝑦𝑥 ¬ 𝑦𝑦 → ∀ 𝑦 𝐴 ¬ 𝑦𝑦 ) )
4 3 rexlimiv ( ∃ 𝑥𝐴𝑦𝑥 ¬ 𝑦𝑦 → ∀ 𝑦 𝐴 ¬ 𝑦𝑦 )