Theorem rexcom 3308

Description: Commutation of restricted existential quantifiers. (Contributed by NM, 19-Nov-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)

Assertion

Ref	Expression
rexcom	⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)

Distinct variable groups:   𝑥,𝑦   𝑥,𝐵   𝑦,𝐴

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑦)

Proof of Theorem rexcom

Step	Hyp	Ref	Expression
1		nfcv 2968	. 2 ⊢ Ⅎ𝑦𝐴
2		nfcv 2968	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	rexcomf 3306	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   ↔ wb 198  ∃wrex 3117

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2390

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clel 2820  df-nfc 2957  df-ral 3121  df-rex 3122

This theorem is referenced by:  rexcom13  3310  rexcom4  3441  iuncom  4746  xpiundi  5405  brdom7disj  9667  addcompr  10157  mulcompr  10159  qmulz  12073  elpq  12096  caubnd2  14473  ello1mpt2  14629  o1lo1  14644  lo1add  14733  lo1mul  14734  rlimno1  14760  sqrt2irr  15351  bezoutlem2  15629  bezoutlem4  15631  pythagtriplem19  15908  lsmcom2  18420  efgrelexlemb  18515  lsmcomx  18611  pgpfac1lem2  18827  pgpfac1lem4  18830  regsep2  21550  ordthaus  21558  tgcmp  21574  txcmplem1  21814  xkococnlem  21832  regr1lem2  21913  dyadmax  23763  coeeu  24379  ostth  25740  axpasch  26239  axeuclidlem  26260  usgr2pth0  27066  elwwlks2  27294  elwspths2spth  27295  shscom  28732  mdsymlem4  29819  mdsymlem8  29823  ordtconnlem1  30514  cvmliftlem15  31825  lshpsmreu  35183  islpln5  35609  islvol5  35653  paddcom  35887  mapdrvallem2  37719  hdmapglem7a  38001  fourierdlem42  41159  2rexsb  41995  2rexrsb  41996  2reurex  42005  2reu1  42010  2reu4a  42013  pgrpgt2nabl  42993  islindeps2  43118  isldepslvec2  43120