Theorem 2ralor

Description: Distribute restricted universal quantification over "or". (Contributed by Jeff Madsen, 19-Jun-2010)

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

Proof

Step	Hyp	Ref	Expression
1		rexnal	|- ( E. x e. A -. ph <-> -. A. x e. A ph )
2		rexnal	|- ( E. y e. B -. ps <-> -. A. y e. B ps )
3	1 2	anbi12i	|- ( ( E. x e. A -. ph /\ E. y e. B -. ps ) <-> ( -. A. x e. A ph /\ -. A. y e. B ps ) )
4		ioran	|- ( -. ( ph \/ ps ) <-> ( -. ph /\ -. ps ) )
5	4	rexbii	|- ( E. y e. B -. ( ph \/ ps ) <-> E. y e. B ( -. ph /\ -. ps ) )
6		rexnal	|- ( E. y e. B -. ( ph \/ ps ) <-> -. A. y e. B ( ph \/ ps ) )
7	5 6	bitr3i	|- ( E. y e. B ( -. ph /\ -. ps ) <-> -. A. y e. B ( ph \/ ps ) )
8	7	rexbii	|- ( E. x e. A E. y e. B ( -. ph /\ -. ps ) <-> E. x e. A -. A. y e. B ( ph \/ ps ) )
9		reeanv	|- ( E. x e. A E. y e. B ( -. ph /\ -. ps ) <-> ( E. x e. A -. ph /\ E. y e. B -. ps ) )
10		rexnal	|- ( E. x e. A -. A. y e. B ( ph \/ ps ) <-> -. A. x e. A A. y e. B ( ph \/ ps ) )
11	8 9 10	3bitr3ri	|- ( -. A. x e. A A. y e. B ( ph \/ ps ) <-> ( E. x e. A -. ph /\ E. y e. B -. ps ) )
12		ioran	|- ( -. ( A. x e. A ph \/ A. y e. B ps ) <-> ( -. A. x e. A ph /\ -. A. y e. B ps ) )
13	3 11 12	3bitr4i	|- ( -. A. x e. A A. y e. B ( ph \/ ps ) <-> -. ( A. x e. A ph \/ A. y e. B ps ) )
14	13	con4bii	|- ( A. x e. A A. y e. B ( ph \/ ps ) <-> ( A. x e. A ph \/ A. y e. B ps ) )