This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem reximdv2

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of Margaris p. 90. (Contributed by NM, 17-Sep-2003)

		Ref	Expression
	Hypothesis	reximdv2.1	$⊢ φ \to ((x \in A \land ψ) \to (x \in B \land χ))$
	Assertion	reximdv2	$⊢ φ \to (\exists x \in A ψ \to \exists x \in B χ)$

Step	Hyp	Ref	Expression
1		reximdv2.1	$⊢ φ \to ((x \in A \land ψ) \to (x \in B \land χ))$
2	1	eximdv	$⊢ φ \to (\exists x (x \in A \land ψ) \to \exists x (x \in B \land χ))$
3		df-rex	$⊢ \exists x \in A ψ \leftrightarrow \exists x (x \in A \land ψ)$
4		df-rex	$⊢ \exists x \in B χ \leftrightarrow \exists x (x \in B \land χ)$
5	2 3 4	3imtr4g	$⊢ φ \to (\exists x \in A ψ \to \exists x \in B χ)$