Metamath Proof Explorer

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	$⊢ φ \to \exists x \in B ψ$
		reximssdv.2	$⊢ (φ \land (x \in B \land ψ)) \to x \in A$
		reximssdv.3	$⊢ (φ \land (x \in B \land ψ)) \to χ$
	Assertion	reximssdv	$⊢ φ \to \exists x \in A χ$

Proof

Step	Hyp	Ref	Expression
1		reximssdv.1	$⊢ φ \to \exists x \in B ψ$
2		reximssdv.2	$⊢ (φ \land (x \in B \land ψ)) \to x \in A$
3		reximssdv.3	$⊢ (φ \land (x \in B \land ψ)) \to χ$
4	2 3	jca	$⊢ (φ \land (x \in B \land ψ)) \to (x \in A \land χ)$
5	4	ex	$⊢ φ \to ((x \in B \land ψ) \to (x \in A \land χ))$
6	5	reximdv2	$⊢ φ \to (\exists x \in B ψ \to \exists x \in A χ)$
7	1 6	mpd	$⊢ φ \to \exists x \in A χ$