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 xAyx¬yyyA¬yy

Proof

Step Hyp Ref Expression
1 intss1 xAAx
2 ssralv Axyx¬yyyA¬yy
3 1 2 syl xAyx¬yyyA¬yy
4 3 rexlimiv xAyx¬yyyA¬yy