Theorem r2ex 2152

Description: Double restricted existential quantification.

Assertion

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

Distinct variable groups:   x,y   y,A

Proof of Theorem r2ex

Step	Hyp	Ref	Expression
1		df-rex 2110	. 2 |- (E.x e. A E.y e. B ph <-> E.x(x e. A /\ E.y e. B ph))
2		19.42v 1688	. . . 4 |- (E.y(x e. A /\ (y e. B /\ ph)) <-> (x e. A /\ E.y(y e. B /\ ph)))
3		anass 487	. . . . 5 |- (((x e. A /\ y e. B) /\ ph) <-> (x e. A /\ (y e. B /\ ph)))
4	3	exbii 1398	. . . 4 |- (E.y((x e. A /\ y e. B) /\ ph) <-> E.y(x e. A /\ (y e. B /\ ph)))
5		df-rex 2110	. . . . 5 |- (E.y e. B ph <-> E.y(y e. B /\ ph))
6	5	anbi2i 538	. . . 4 |- ((x e. A /\ E.y e. B ph) <-> (x e. A /\ E.y(y e. B /\ ph)))
7	2, 4, 6	3bitr4i 200	. . 3 |- (E.y((x e. A /\ y e. B) /\ ph) <-> (x e. A /\ E.y e. B ph))
8	7	exbii 1398	. 2 |- (E.xE.y((x e. A /\ y e. B) /\ ph) <-> E.x(x e. A /\ E.y e. B ph))
9	1, 8	bitr4i 193	1 |- (E.x e. A E.y e. B ph <-> E.xE.y((x e. A /\ y e. B) /\ ph))

Syntax hints:   <-> wb 163   /\ wa 240   e. wcel 1300  E.wex 1326  E.wrex 2106

This theorem is referenced by:  rexcom 2243  reean 2247  genpv 6254  axcnre 6439  pjtheui 10868  pjpj0i 10888  spanuni 11100  osumlem7 11219  5oalem7 11240  3oalem3 11244  rnoprab2 13842  rngop 14484  bsi 14845

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-rex 2110

Copyright terms: Public domain