This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ssuni

Description: Subclass relationship for class union. (Contributed by NM, 24-May-1994) (Proof shortened by Andrew Salmon, 29-Jun-2011) (Proof shortened by JJ, 26-Jul-2021)

Ref Expression
Assertion ssuni 
|- ( ( A C_ B /\ B e. C ) -> A C_ U. C )

Proof

Step Hyp Ref Expression
1 elunii 
 |-  ( ( x e. B /\ B e. C ) -> x e. U. C )
2 1 expcom 
 |-  ( B e. C -> ( x e. B -> x e. U. C ) )
3 2 imim2d 
 |-  ( B e. C -> ( ( x e. A -> x e. B ) -> ( x e. A -> x e. U. C ) ) )
4 3 alimdv 
 |-  ( B e. C -> ( A. x ( x e. A -> x e. B ) -> A. x ( x e. A -> x e. U. C ) ) )
5 df-ss 
 |-  ( A C_ B <-> A. x ( x e. A -> x e. B ) )
6 df-ss 
 |-  ( A C_ U. C <-> A. x ( x e. A -> x e. U. C ) )
7 4 5 6 3imtr4g 
 |-  ( B e. C -> ( A C_ B -> A C_ U. C ) )
8 7 impcom 
 |-  ( ( A C_ B /\ B e. C ) -> A C_ U. C )