Theorem raaan

Description: Rearrange restricted quantifiers. (Contributed by NM, 26-Oct-2010)

	Ref	Expression
Hypotheses	raaan.1	|- F/ y ph
	raaan.2	|- F/ x ps
Assertion	raaan	|- ( A. x e. A A. y e. A ( ph /\ ps ) <-> ( A. x e. A ph /\ A. y e. A ps ) )

Proof

Step	Hyp	Ref	Expression
1		raaan.1	|- F/ y ph
2		raaan.2	|- F/ x ps
3		rzal	|- ( A = (/) -> A. x e. A A. y e. A ( ph /\ ps ) )
4		rzal	|- ( A = (/) -> A. x e. A ph )
5		rzal	|- ( A = (/) -> A. y e. A ps )
6		pm5.1	|- ( ( A. x e. A A. y e. A ( ph /\ ps ) /\ ( A. x e. A ph /\ A. y e. A ps ) ) -> ( A. x e. A A. y e. A ( ph /\ ps ) <-> ( A. x e. A ph /\ A. y e. A ps ) ) )
7	3 4 5 6	syl12anc	|- ( A = (/) -> ( A. x e. A A. y e. A ( ph /\ ps ) <-> ( A. x e. A ph /\ A. y e. A ps ) ) )
8	1	r19.28z	|- ( A =/= (/) -> ( A. y e. A ( ph /\ ps ) <-> ( ph /\ A. y e. A ps ) ) )
9	8	ralbidv	|- ( A =/= (/) -> ( A. x e. A A. y e. A ( ph /\ ps ) <-> A. x e. A ( ph /\ A. y e. A ps ) ) )
10		nfcv	|- F/_ x A
11	10 2	nfralw	|- F/ x A. y e. A ps
12	11	r19.27z	|- ( A =/= (/) -> ( A. x e. A ( ph /\ A. y e. A ps ) <-> ( A. x e. A ph /\ A. y e. A ps ) ) )
13	9 12	bitrd	|- ( A =/= (/) -> ( A. x e. A A. y e. A ( ph /\ ps ) <-> ( A. x e. A ph /\ A. y e. A ps ) ) )
14	7 13	pm2.61ine	|- ( A. x e. A A. y e. A ( ph /\ ps ) <-> ( A. x e. A ph /\ A. y e. A ps ) )