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

Metamath Proof Explorer

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 x y \in A$
	hbral.2	$⊢ φ \to \forall x φ$
Assertion	hbral	$⊢ \forall y \in A φ \to \forall x \forall y \in A φ$

Proof

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