Theorem reeanv 1781

Description: Rearrange existential quantifiers.

Assertion

Ref	Expression
reeanv	|- (E.x e. A E.y e. B (ph /\ ps) <-> (E.x e. A ph /\ E.y e. B ps))

Distinct variable groups:   ph,y   ps,x   x,y   y,A   x,B

Proof of Theorem reeanv

Step	Hyp	Ref	Expression
1		anass 441	. . . . 5 |- (((x e. A /\ y e. B) /\ (ph /\ ps)) <-> (x e. A /\ (y e. B /\ (ph /\ ps))))
2		an4 508	. . . . 5 |- (((x e. A /\ y e. B) /\ (ph /\ ps)) <-> ((x e. A /\ ph) /\ (y e. B /\ ps)))
3	1, 2	bitr3 175	. . . 4 |- ((x e. A /\ (y e. B /\ (ph /\ ps))) <-> ((x e. A /\ ph) /\ (y e. B /\ ps)))
4	3	2exbii 1054	. . 3 |- (E.xE.y(x e. A /\ (y e. B /\ (ph /\ ps))) <-> E.xE.y((x e. A /\ ph) /\ (y e. B /\ ps)))
5		exdistr 1311	. . 3 |- (E.xE.y(x e. A /\ (y e. B /\ (ph /\ ps))) <-> E.x(x e. A /\ E.y(y e. B /\ (ph /\ ps))))
6		eeanv 1325	. . 3 |- (E.xE.y((x e. A /\ ph) /\ (y e. B /\ ps)) <-> (E.x(x e. A /\ ph) /\ E.y(y e. B /\ ps)))
7	4, 5, 6	3bitr3 181	. 2 |- (E.x(x e. A /\ E.y(y e. B /\ (ph /\ ps))) <-> (E.x(x e. A /\ ph) /\ E.y(y e. B /\ ps)))
8		df-rex 1653	. . . 4 |- (E.y e. B (ph /\ ps) <-> E.y(y e. B /\ (ph /\ ps)))
9	8	rexbii 1671	. . 3 |- (E.x e. A E.y e. B (ph /\ ps) <-> E.x e. A E.y(y e. B /\ (ph /\ ps)))
10		df-rex 1653	. . 3 |- (E.x e. A E.y(y e. B /\ (ph /\ ps)) <-> E.x(x e. A /\ E.y(y e. B /\ (ph /\ ps))))
11	9, 10	bitr 173	. 2 |- (E.x e. A E.y e. B (ph /\ ps) <-> E.x(x e. A /\ E.y(y e. B /\ (ph /\ ps))))
12		df-rex 1653	. . 3 |- (E.x e. A ph <-> E.x(x e. A /\ ph))
13		df-rex 1653	. . 3 |- (E.y e. B ps <-> E.y(y e. B /\ ps))
14	12, 13	anbi12i 484	. 2 |- ((E.x e. A ph /\ E.y e. B ps) <-> (E.x(x e. A /\ ph) /\ E.y(y e. B /\ ps)))
15	7, 11, 14	3bitr4 183	1 |- (E.x e. A E.y e. B (ph /\ ps) <-> (E.x e. A ph /\ E.y e. B ps))

Syntax hints:   <-> wb 146   /\ wa 223   e. wcel 960  E.wex 982  E.wrex 1649

This theorem is referenced by:  tfrlem5 3921  unfi 4563  unfiOLD 4564  rankxplim3 4724  kmlem9 4783  cvganz 6924  climunii 7098  climaddlem3 7116  climmullem8 7127  infxpidmlem7 7559  tgclt 7623  opnin 7866  xplm 7972  xpcn 7973  hlimunii 9103  pjtheu 9230  pjpj0 9250  superpos 10276  irred 10316  cdjreu 10354  cdj3 10363  ghomgrpilem2 10381

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-rex 1653

Copyright terms: Public domain