Theorem hbral

Description: Bound-variable hypothesis builder for restricted quantification. (Contributed by NM, 1-Sep-1999) (Revised by David Abernethy, 13-Dec-2009)

	Ref	Expression
Hypotheses	hbral.1	$$⊢y\in A\to \forall xy\in A$$
	hbral.2	$$⊢\phi \to \forall x\phi$$
Assertion	hbral	$$⊢\forall y\in A\phi \to \forall x\forall y\in A\phi$$

Proof

Step	Hyp	Ref	Expression
1		hbral.1	$$⊢y\in A\to \forall xy\in A$$
2		hbral.2	$$⊢\phi \to \forall x\phi$$
3		df-ral	$$⊢\forall y\in A\phi \leftrightarrow \forall y\left(y\in A\to \phi \right)$$
4	1 2	hbim	$$⊢\left(y\in A\to \phi \right)\to \forall x\left(y\in A\to \phi \right)$$
5	4	hbal	$$⊢\forall y\left(y\in A\to \phi \right)\to \forall x\forall y\left(y\in A\to \phi \right)$$
6	3 5	hbxfrbi	$$⊢\forall y\in A\phi \to \forall x\forall y\in A\phi$$