Theorem r2ex 2977

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 2832	. 2 |- ( A. x e. A A. y e. B -. ph <-> A. x A. y ( ( x e. A /\ y e. B ) -> -. ph ) )
2	1	r2exlem 2974	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 184   /\ wa 367   E.wex 1617   e. wcel 1823   E.wrex 2805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709

This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-ral 2809  df-rex 2810

This theorem is referenced by:  reean  3021  rnoprab2  6359  elrnmpt2res  6389  oeeu  7244  omxpenlem  7611  axcnre  9530  hash2prv  12509  hash2sspr  12510  pmtrrn2  16684  fsumvma  23686  usgrarnedg  24586  spanuni  26660  5oalem7  26776  3oalem3  26780  elfuns  29793  ellines  30030  usgedgimp  32775  usgedgimpALT  32778  dalem20  35814  diblsmopel  37295  iunrelexpuztr  38206