Metamath Proof Explorer

Theorem ssexg

Description: The subset of a set is also a set. Exercise 3 of TakeutiZaring p. 22 (generalized). (Contributed by NM, 14-Aug-1994)

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

Proof

Step Hyp Ref Expression
1 sseq2 
 |-  ( x = B -> ( A C_ x <-> A C_ B ) )
2 1 imbi1d 
 |-  ( x = B -> ( ( A C_ x -> A e. _V ) <-> ( A C_ B -> A e. _V ) ) )
3 vex 
 |-  x e. _V
4 3 ssex 
 |-  ( A C_ x -> A e. _V )
5 2 4 vtoclg 
 |-  ( B e. C -> ( A C_ B -> A e. _V ) )
6 5 impcom 
 |-  ( ( A C_ B /\ B e. C ) -> A e. _V )