Metamath Proof Explorer


Theorem intssuni

Description: The intersection of a nonempty set is a subclass of its union. (Contributed by NM, 29-Jul-2006)

Ref Expression
Assertion intssuni A A A

Proof

Step Hyp Ref Expression
1 r19.2z A y A x y y A x y
2 1 ex A y A x y y A x y
3 vex x V
4 3 elint2 x A y A x y
5 eluni2 x A y A x y
6 2 4 5 3imtr4g A x A x A
7 6 ssrdv A A A