Theorem r2ex 3061

Description: Double restricted existential quantification. (Contributed by NM, 11-Nov-1995.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 10-Jan-2020.)

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		r2al 2939	. 2 |- ( A. x e. A A. y e. B -. ph <-> A. x A. y ( ( x e. A /\ y e. B ) -> -. ph ) )
2	1	r2exlem 3059	1 |- ( E. x e. A E. y e. B ph <-> E. x E. y ( ( x e. A /\ y e. B ) /\ ph ) )

Syntax hints:   -. wn 3   <-> wb 196   /\ wa 384   E.wex 1704   e. wcel 1990   E.wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-ral 2917  df-rex 2918

This theorem is referenced by:  reean  3106  elxp2  5132  rnoprab2  6744  elrnmpt2res  6774  oeeu  7683  omxpenlem  8061  axcnre  9985  hash2prb  13254  hashle2prv  13260  pmtrrn2  17880  fsumvma  24938  umgredg  26033  fusgr2wsp2nb  27198  spanuni  28403  5oalem7  28519  3oalem3  28523  elfuns  32022  ellines  32259  dalem20  34979  diblsmopel  36460  iunrelexpuztr  38011  sprssspr  41731