Metamath Proof Explorer

Theorem ssrexv

Description: Existential quantification restricted to a subclass. (Contributed by NM, 11-Jan-2007) Avoid axioms. (Revised by GG, 19-May-2025)

Ref Expression
Assertion ssrexv 
|- ( A C_ B -> ( E. x e. A ph -> E. x e. B ph ) )

Proof

Step Hyp Ref Expression
1 df-ss 
 |-  ( A C_ B <-> A. x ( x e. A -> x e. B ) )
2 pm3.45 
 |-  ( ( x e. A -> x e. B ) -> ( ( x e. A /\ ph ) -> ( x e. B /\ ph ) ) )
3 2 aleximi 
 |-  ( A. x ( x e. A -> x e. B ) -> ( E. x ( x e. A /\ ph ) -> E. x ( x e. B /\ ph ) ) )
4 df-rex 
 |-  ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
5 df-rex 
 |-  ( E. x e. B ph <-> E. x ( x e. B /\ ph ) )
6 3 4 5 3imtr4g 
 |-  ( A. x ( x e. A -> x e. B ) -> ( E. x e. A ph -> E. x e. B ph ) )
7 1 6 sylbi 
 |-  ( A C_ B -> ( E. x e. A ph -> E. x e. B ph ) )