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 x A y x ¬ y y y A ¬ y y

Proof

Step Hyp Ref Expression
1 intss1 x A A x
2 ssralv A x y x ¬ y y y A ¬ y y
3 1 2 syl x A y x ¬ y y y A ¬ y y
4 3 rexlimiv x A y x ¬ y y y A ¬ y y