Theorem reximssdv

Description: Derivation of a restricted existential quantification over a subset (the second hypothesis implies A C_ B ), deduction form. (Contributed by AV, 21-Aug-2022)

	Ref	Expression
Hypotheses	reximssdv.1	|- ( ph -> E. x e. B ps )
	reximssdv.2	|- ( ( ph /\ ( x e. B /\ ps ) ) -> x e. A )
	reximssdv.3	|- ( ( ph /\ ( x e. B /\ ps ) ) -> ch )
Assertion	reximssdv	|- ( ph -> E. x e. A ch )

Proof

Step	Hyp	Ref	Expression
1		reximssdv.1	|- ( ph -> E. x e. B ps )
2		reximssdv.2	|- ( ( ph /\ ( x e. B /\ ps ) ) -> x e. A )
3		reximssdv.3	|- ( ( ph /\ ( x e. B /\ ps ) ) -> ch )
4	2 3	jca	|- ( ( ph /\ ( x e. B /\ ps ) ) -> ( x e. A /\ ch ) )
5	4	ex	|- ( ph -> ( ( x e. B /\ ps ) -> ( x e. A /\ ch ) ) )
6	5	reximdv2	|- ( ph -> ( E. x e. B ps -> E. x e. A ch ) )
7	1 6	mpd	|- ( ph -> E. x e. A ch )