Theorem reeanv 1770

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 505	. . . . 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 1048	. . 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 1304	. . 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 1318	. . 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 1642	. . . 4 |- (E.y e. B (ph /\ ps) <-> E.y(y e. B /\ (ph /\ ps)))
9	8	rexbii 1660	. . 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 1642	. . 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 1642	. . 3 |- (E.x e. A ph <-> E.x(x e. A /\ ph))
13		df-rex 1642	. . 3 |- (E.y e. B ps <-> E.y(y e. B /\ ps))
14	12, 13	anbi12i 481	. 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 955  E.wex 977  E.wrex 1638

This theorem is referenced by:  tfrlem5 3900  unfi 4528  rankxplim3 4686  kmlem9 4745  cvganz 6861  climunii 7035  climaddlem3 7052  climmullem8 7063  infxpidmlem7 7501  tgclt 7566  opnin 7809  xplm 7909  xpcn 7910  hlimunii 9029  pjtheu 9150  pjpj0 9170  superpos 10189  irred 10229  cdjreu 10264  cdj3 10273  ghomgrpilem2 10291

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975

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

Copyright terms: Public domain