Theorem 2reu5lem2

Description: Lemma for 2reu5 . (Contributed by Alexander van der Vekens, 17-Jun-2017)

	Ref	Expression
Assertion	2reu5lem2	|- ( A. x e. A E* y e. B ph <-> A. x E* y ( x e. A /\ y e. B /\ ph ) )

Proof

Step	Hyp	Ref	Expression
1		df-rmo	|- ( E* y e. B ph <-> E* y ( y e. B /\ ph ) )
2	1	ralbii	|- ( A. x e. A E* y e. B ph <-> A. x e. A E* y ( y e. B /\ ph ) )
3		df-ral	|- ( A. x e. A E* y ( y e. B /\ ph ) <-> A. x ( x e. A -> E* y ( y e. B /\ ph ) ) )
4		moanimv	|- ( E* y ( x e. A /\ ( y e. B /\ ph ) ) <-> ( x e. A -> E* y ( y e. B /\ ph ) ) )
5	4	bicomi	|- ( ( x e. A -> E* y ( y e. B /\ ph ) ) <-> E* y ( x e. A /\ ( y e. B /\ ph ) ) )
6		3anass	|- ( ( x e. A /\ y e. B /\ ph ) <-> ( x e. A /\ ( y e. B /\ ph ) ) )
7	6	bicomi	|- ( ( x e. A /\ ( y e. B /\ ph ) ) <-> ( x e. A /\ y e. B /\ ph ) )
8	7	mobii	|- ( E* y ( x e. A /\ ( y e. B /\ ph ) ) <-> E* y ( x e. A /\ y e. B /\ ph ) )
9	5 8	bitri	|- ( ( x e. A -> E* y ( y e. B /\ ph ) ) <-> E* y ( x e. A /\ y e. B /\ ph ) )
10	9	albii	|- ( A. x ( x e. A -> E* y ( y e. B /\ ph ) ) <-> A. x E* y ( x e. A /\ y e. B /\ ph ) )
11	3 10	bitri	|- ( A. x e. A E* y ( y e. B /\ ph ) <-> A. x E* y ( x e. A /\ y e. B /\ ph ) )
12	2 11	bitri	|- ( A. x e. A E* y e. B ph <-> A. x E* y ( x e. A /\ y e. B /\ ph ) )