Theorem reeanv 1778

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 439	. . . . 5 |- (((x e. A /\ y e. B) /\ (ph /\ ps)) <-> (x e. A /\ (y e. B /\ (ph /\ ps))))
2		an4 506	. . . . 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 1052	. . 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 1309	. . 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 1323	. . 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 1650	. . . 4 |- (E.y e. B (ph /\ ps) <-> E.y(y e. B /\ (ph /\ ps)))
9	8	rexbii 1668	. . 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 1650	. . 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 1650	. . 3 |- (E.x e. A ph <-> E.x(x e. A /\ ph))
13		df-rex 1650	. . 3 |- (E.y e. B ps <-> E.y(y e. B /\ ps))
14	12, 13	anbi12i 482	. 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 958  E.wex 980  E.wrex 1646

This theorem is referenced by:  tfrlem5 3915  unfi 4551  unfiOLD 4552  rankxplim3 4714  kmlem9 4773  cvganz 6924  climunii 7098  climaddlem3 7116  climmullem8 7127  infxpidmlem7 7558  tgclt 7624  opnin 7869  xplm 7975  xpcn 7976  hlimunii 9108  pjtheu 9235  pjpj0 9255  superpos 10281  irred 10321  cdjreu 10359  cdj3 10368  ghomgrpilem2 10386

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978

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

Copyright terms: Public domain