Metamath Proof Explorer

Theorem ss2ralv

Description: Two quantifications restricted to a subclass. (Contributed by AV, 11-Mar-2023)

Ref Expression
Assertion ss2ralv 
|- ( A C_ B -> ( A. x e. B A. y e. B ph -> A. x e. A A. y e. A ph ) )

Proof

Step Hyp Ref Expression
1 ssralv 
 |-  ( A C_ B -> ( A. y e. B ph -> A. y e. A ph ) )
2 1 ralimdv 
 |-  ( A C_ B -> ( A. x e. B A. y e. B ph -> A. x e. B A. y e. A ph ) )
3 ssralv 
 |-  ( A C_ B -> ( A. x e. B A. y e. A ph -> A. x e. A A. y e. A ph ) )
4 2 3 syld 
 |-  ( A C_ B -> ( A. x e. B A. y e. B ph -> A. x e. A A. y e. A ph ) )