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

Metamath Proof Explorer

Theorem unss

Description: The union of two subclasses is a subclass. Theorem 27 of Suppes p. 27 and its converse. (Contributed by NM, 11-Jun-2004)

Ref Expression
Assertion unss 
|- ( ( A C_ C /\ B C_ C ) <-> ( A u. B ) C_ C )

Proof

Step Hyp Ref Expression
1 df-ss 
 |-  ( ( A u. B ) C_ C <-> A. x ( x e. ( A u. B ) -> x e. C ) )
2 19.26 
 |-  ( A. x ( ( x e. A -> x e. C ) /\ ( x e. B -> x e. C ) ) <-> ( A. x ( x e. A -> x e. C ) /\ A. x ( x e. B -> x e. C ) ) )
3 elunant 
 |-  ( ( x e. ( A u. B ) -> x e. C ) <-> ( ( x e. A -> x e. C ) /\ ( x e. B -> x e. C ) ) )
4 3 albii 
 |-  ( A. x ( x e. ( A u. B ) -> x e. C ) <-> A. x ( ( x e. A -> x e. C ) /\ ( x e. B -> x e. C ) ) )
5 df-ss 
 |-  ( A C_ C <-> A. x ( x e. A -> x e. C ) )
6 df-ss 
 |-  ( B C_ C <-> A. x ( x e. B -> x e. C ) )
7 5 6 anbi12i 
 |-  ( ( A C_ C /\ B C_ C ) <-> ( A. x ( x e. A -> x e. C ) /\ A. x ( x e. B -> x e. C ) ) )
8 2 4 7 3bitr4i 
 |-  ( A. x ( x e. ( A u. B ) -> x e. C ) <-> ( A C_ C /\ B C_ C ) )
9 1 8 bitr2i 
 |-  ( ( A C_ C /\ B C_ C ) <-> ( A u. B ) C_ C )