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 e. A -> A. x y e. A )
	hbral.2	|- ( ph -> A. x ph )
Assertion	hbral	|- ( A. y e. A ph -> A. x A. y e. A ph )

Proof

Step	Hyp	Ref	Expression
1		hbral.1	|- ( y e. A -> A. x y e. A )
2		hbral.2	|- ( ph -> A. x ph )
3		df-ral	|- ( A. y e. A ph <-> A. y ( y e. A -> ph ) )
4	1 2	hbim	|- ( ( y e. A -> ph ) -> A. x ( y e. A -> ph ) )
5	4	hbal	|- ( A. y ( y e. A -> ph ) -> A. x A. y ( y e. A -> ph ) )
6	3 5	hbxfrbi	|- ( A. y e. A ph -> A. x A. y e. A ph )