Theorem r2ex 2872

Description: Double restricted existential quantification. (Contributed by NM, 11-Nov-1995.)

Assertion

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

Distinct variable groups:   x, y   y, A

Allowed substitution hints:   ph( x, y)   A( x)   B( x, y)

Proof of Theorem r2ex

Step	Hyp	Ref	Expression
1		nfcv 2614	. 2 |- F/_ y A
2	1	r2exf 2870	1 |- ( E. x e. A E. y e. B ph <-> E. x E. y ( ( x e. A /\ y e. B ) /\ ph ) )

Syntax hints:   <-> wb 184   /\ wa 369   E.wex 1587   e. wcel 1758   E.wrex 2797

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1954  ax-ext 2431

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1588  df-nf 1591  df-sb 1703  df-cleq 2444  df-clel 2447  df-nfc 2602  df-rex 2802

This theorem is referenced by:  reean  2987  rnoprab2  6279  elrnmpt2res  6309  oeeu  7147  omxpenlem  7517  axcnre  9437  pmtrrn2  16080  fsumvma  22680  usgrarnedg  23450  spanuni  25094  5oalem7  25210  3oalem3  25214  elfuns  28085  ellines  28322  hash2prv  30369  hash2sspr  30370  dalem20  33656  diblsmopel  35135