Metamath Proof Explorer

Theorem reximd2a

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of Margaris p. 90. (Contributed by Thierry Arnoux, 27-Jan-2020)

		Ref	Expression
	Hypotheses	reximd2a.1	$⊢ Ⅎ x φ$
		reximd2a.2	$⊢ ((φ \land x \in A) \land ψ) \to x \in B$
		reximd2a.3	$⊢ ((φ \land x \in A) \land ψ) \to χ$
		reximd2a.4	$⊢ φ \to \exists x \in A ψ$
	Assertion	reximd2a	$⊢ φ \to \exists x \in B χ$

Proof

Step	Hyp	Ref	Expression
1		reximd2a.1	$⊢ Ⅎ x φ$
2		reximd2a.2	$⊢ ((φ \land x \in A) \land ψ) \to x \in B$
3		reximd2a.3	$⊢ ((φ \land x \in A) \land ψ) \to χ$
4		reximd2a.4	$⊢ φ \to \exists x \in A ψ$
5	2 3	jca	$⊢ ((φ \land x \in A) \land ψ) \to (x \in B \land χ)$
6	5	expl	$⊢ φ \to ((x \in A \land ψ) \to (x \in B \land χ))$
7	1 6	eximd	$⊢ φ \to (\exists x (x \in A \land ψ) \to \exists x (x \in B \land χ))$
8		df-rex	$⊢ \exists x \in A ψ \leftrightarrow \exists x (x \in A \land ψ)$
9		df-rex	$⊢ \exists x \in B χ \leftrightarrow \exists x (x \in B \land χ)$
10	7 8 9	3imtr4g	$⊢ φ \to (\exists x \in A ψ \to \exists x \in B χ)$
11	4 10	mpd	$⊢ φ \to \exists x \in B χ$