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

Metamath Proof Explorer

Theorem ralimi2

Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 22-Feb-2004)

		Ref	Expression
	Hypothesis	ralimi2.1	$⊢ (x \in A \to φ) \to (x \in B \to ψ)$
	Assertion	ralimi2	$⊢ \forall x \in A φ \to \forall x \in B ψ$

Step	Hyp	Ref	Expression
1		ralimi2.1	$⊢ (x \in A \to φ) \to (x \in B \to ψ)$
2	1	alimi	$⊢ \forall x (x \in A \to φ) \to \forall x (x \in B \to ψ)$
3		df-ral	$⊢ \forall x \in A φ \leftrightarrow \forall x (x \in A \to φ)$
4		df-ral	$⊢ \forall x \in B ψ \leftrightarrow \forall x (x \in B \to ψ)$
5	2 3 4	3imtr4i	$⊢ \forall x \in A φ \to \forall x \in B ψ$