Theorem r19.26-2

Description: Restricted quantifier version of 19.26-2 . Version of r19.26 with two quantifiers. (Contributed by NM, 10-Aug-2004)

	Ref	Expression
Assertion	r19.26-2	|- ( A. x e. A A. y e. B ( ph /\ ps ) <-> ( A. x e. A A. y e. B ph /\ A. x e. A A. y e. B ps ) )

Proof

Step	Hyp	Ref	Expression
1		r19.26	|- ( A. y e. B ( ph /\ ps ) <-> ( A. y e. B ph /\ A. y e. B ps ) )
2	1	ralbii	|- ( A. x e. A A. y e. B ( ph /\ ps ) <-> A. x e. A ( A. y e. B ph /\ A. y e. B ps ) )
3		r19.26	|- ( A. x e. A ( A. y e. B ph /\ A. y e. B ps ) <-> ( A. x e. A A. y e. B ph /\ A. x e. A A. y e. B ps ) )
4	2 3	bitri	|- ( A. x e. A A. y e. B ( ph /\ ps ) <-> ( A. x e. A A. y e. B ph /\ A. x e. A A. y e. B ps ) )