Metamath Proof Explorer

Theorem intss

Description: Intersection of subclasses. (Contributed by NM, 14-Oct-1999) (Proof shortened by OpenAI, 25-Mar-2020)

Ref Expression
Assertion intss 
|- ( A C_ B -> |^| B C_ |^| A )

Proof

Step Hyp Ref Expression
1 ssralv 
 |-  ( A C_ B -> ( A. x e. B y e. x -> A. x e. A y e. x ) )
2 1 ss2abdv 
 |-  ( A C_ B -> { y | A. x e. B y e. x } C_ { y | A. x e. A y e. x } )
3 dfint2 
 |-  |^| B = { y | A. x e. B y e. x }
4 dfint2 
 |-  |^| A = { y | A. x e. A y e. x }
5 2 3 4 3sstr4g 
 |-  ( A C_ B -> |^| B C_ |^| A )