Theorem rexcom 3080

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 2751	. 2 ⊢ Ⅎ𝑦𝐴
2		nfcv 2751	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	rexcomf 3078	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   ↔ wb 195  ∃wrex 2897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902

This theorem is referenced by:  rexcom13  3081  rexcom4  3198  iuncom  4463  xpiundi  5096  brdom7disj  9234  addcompr  9722  mulcompr  9724  qmulz  11667  caubnd2  13945  ello1mpt2  14101  o1lo1  14116  lo1add  14205  lo1mul  14206  rlimno1  14232  sqrt2irr  14817  bezoutlem2  15095  bezoutlem4  15097  pythagtriplem19  15376  lsmcom2  17893  efgrelexlemb  17986  lsmcomx  18082  pgpfac1lem2  18297  pgpfac1lem4  18300  regsep2  20990  ordthaus  20998  tgcmp  21014  txcmplem1  21254  xkococnlem  21272  regr1lem2  21353  dyadmax  23172  coeeu  23785  ostth  25128  axpasch  25621  axeuclidlem  25642  el2wlksot  26407  el2pthsot  26408  frgrawopreglem5  26575  shscom  27562  mdsymlem4  28649  mdsymlem8  28653  ordtconlem1  29298  cvmliftlem15  30534  nofulllem5  31105  lshpsmreu  33414  islpln5  33839  islvol5  33883  paddcom  34117  mapdrvallem2  35952  hdmapglem7a  36237  fourierdlem42  39042  2rexsb  39819  2rexrsb  39820  2reurex  39830  2reu1  39835  2reu4a  39838  usgr2pth0  40971  elwwlks2  41170  elwspths2spth  41171  frgrwopreglem5  41485  pgrpgt2nabl  41941  islindeps2  42066  isldepslvec2  42068