Metamath Proof Explorer

Theorem ssintab

Description: Subclass of the intersection of a class abstraction. (Contributed by NM, 31-Jul-2006) (Proof shortened by Andrew Salmon, 9-Jul-2011)

Ref Expression
Assertion ssintab 
|- ( A C_ |^| { x | ph } <-> A. x ( ph -> A C_ x ) )

Proof

Step Hyp Ref Expression
1 ssint 
 |-  ( A C_ |^| { x | ph } <-> A. y e. { x | ph } A C_ y )
2 sseq2 
 |-  ( y = x -> ( A C_ y <-> A C_ x ) )
3 2 ralab2 
 |-  ( A. y e. { x | ph } A C_ y <-> A. x ( ph -> A C_ x ) )
4 1 3 bitri 
 |-  ( A C_ |^| { x | ph } <-> A. x ( ph -> A C_ x ) )