Metamath Proof Explorer


Theorem disjss1

Description: A subset of a disjoint collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016)

Ref Expression
Assertion disjss1 ABDisjxBCDisjxAC

Proof

Step Hyp Ref Expression
1 ssel ABxAxB
2 1 anim1d ABxAyCxByC
3 2 moimdv AB*xxByC*xxAyC
4 3 alimdv ABy*xxByCy*xxAyC
5 dfdisj2 DisjxBCy*xxByC
6 dfdisj2 DisjxACy*xxAyC
7 4 5 6 3imtr4g ABDisjxBCDisjxAC