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	⊢ ( 𝑦 ∈ 𝐴 → ∀ 𝑥 𝑦 ∈ 𝐴 )
	hbral.2	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
Assertion	hbral	⊢ ( ∀ 𝑦 ∈ 𝐴 𝜑 → ∀ 𝑥 ∀ 𝑦 ∈ 𝐴 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		hbral.1	⊢ ( 𝑦 ∈ 𝐴 → ∀ 𝑥 𝑦 ∈ 𝐴 )
2		hbral.2	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
3		df-ral	⊢ ( ∀ 𝑦 ∈ 𝐴 𝜑 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → 𝜑 ) )
4	1 2	hbim	⊢ ( ( 𝑦 ∈ 𝐴 → 𝜑 ) → ∀ 𝑥 ( 𝑦 ∈ 𝐴 → 𝜑 ) )
5	4	hbal	⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝐴 → 𝜑 ) → ∀ 𝑥 ∀ 𝑦 ( 𝑦 ∈ 𝐴 → 𝜑 ) )
6	3 5	hbxfrbi	⊢ ( ∀ 𝑦 ∈ 𝐴 𝜑 → ∀ 𝑥 ∀ 𝑦 ∈ 𝐴 𝜑 )