Theorem rexcom 3308

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

Assertion

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

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

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

Proof of Theorem rexcom

Step	Hyp	Ref	Expression
1		df-rex 3112	. . 3 ⊢ (∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜑))
2	1	rexbii 3210	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜑))
3		rexcom4 3212	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜑) ↔ ∃𝑦∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 ∧ 𝜑))
4		r19.42v 3303	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 ∧ 𝜑) ↔ (𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑))
5	4	exbii 1849	. . 3 ⊢ (∃𝑦∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 ∧ 𝜑) ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑))
6		df-rex 3112	. . 3 ⊢ (∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑))
7	5, 6	bitr4i 281	. 2 ⊢ (∃𝑦∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 ∧ 𝜑) ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)
8	2, 3, 7	3bitri 300	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   ↔ wb 209   ∧ wa 399  ∃wex 1781   ∈ wcel 2111  ∃wrex 3107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-11 2158

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-rex 3112

This theorem is referenced by:  rexcom13  3313  rexcom4OLD  3473  2reurex  3698  2reu1  3826  2reu4lem  4423  iuncom  4888  xpiundi  5586  brdom7disj  9942  addcompr  10432  mulcompr  10434  qmulz  12339  elpq  12362  caubnd2  14709  ello1mpt2  14871  o1lo1  14886  lo1add  14975  lo1mul  14976  rlimno1  15002  sqrt2irr  15594  bezoutlem2  15878  bezoutlem4  15880  pythagtriplem19  16160  lsmcom2  18772  efgrelexlemb  18868  lsmcomx  18969  pgpfac1lem2  19190  pgpfac1lem4  19193  regsep2  21981  ordthaus  21989  tgcmp  22006  txcmplem1  22246  xkococnlem  22264  regr1lem2  22345  dyadmax  24202  coeeu  24822  ostth  26223  axpasch  26735  axeuclidlem  26756  usgr2pth0  27554  elwwlks2  27752  elwspths2spth  27753  shscom  29102  mdsymlem4  30189  mdsymlem8  30193  ordtconnlem1  31277  cvmliftlem15  32658  fvineqsneq  34829  lshpsmreu  36405  islpln5  36831  islvol5  36875  paddcom  37109  mapdrvallem2  38941  hdmapglem7a  39223  fsuppind  39456  fourierdlem42  42791  2rexsb  43656  2rexrsb  43657  pgrpgt2nabl  44768  islindeps2  44892  isldepslvec2  44894