Theorem ralimi2

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

	Ref	Expression
Hypothesis	ralimi2.1	$$⊢\left(x\in A\to \phi \right)\to \left(x\in B\to \psi \right)$$
Assertion	ralimi2	$$⊢\forall x\in A\phi \to \forall x\in B\psi$$

Proof

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