Theorem rexcom 3281

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 3069	. . 3 ⊢ (∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜑))
2	1	rexbii 3177	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜑))
3		rexcom4 3179	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜑) ↔ ∃𝑦∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 ∧ 𝜑))
4		r19.42v 3276	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 ∧ 𝜑) ↔ (𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑))
5	4	exbii 1851	. . 3 ⊢ (∃𝑦∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 ∧ 𝜑) ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑))
6		df-rex 3069	. . 3 ⊢ (∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑))
7	5, 6	bitr4i 277	. 2 ⊢ (∃𝑦∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 ∧ 𝜑) ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)
8	2, 3, 7	3bitri 296	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   ↔ wb 205   ∧ wa 395  ∃wex 1783   ∈ wcel 2108  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-11 2156

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-rex 3069

This theorem is referenced by:  rexcom13  3285  2reurex  3690  2reu1  3826  2reu4lem  4453  iuncom  4928  xpiundi  5648  brdom7disj  10218  addcompr  10708  mulcompr  10710  qmulz  12620  elpq  12644  caubnd2  14997  ello1mpt2  15159  o1lo1  15174  lo1add  15264  lo1mul  15265  rlimno1  15293  sqrt2irr  15886  bezoutlem2  16176  bezoutlem4  16178  pythagtriplem19  16462  lsmcom2  19175  efgrelexlemb  19271  lsmcomx  19372  pgpfac1lem2  19593  pgpfac1lem4  19596  regsep2  22435  ordthaus  22443  tgcmp  22460  txcmplem1  22700  xkococnlem  22718  regr1lem2  22799  dyadmax  24667  coeeu  25291  ostth  26692  axpasch  27212  axeuclidlem  27233  usgr2pth0  28034  elwwlks2  28232  elwspths2spth  28233  shscom  29582  mdsymlem4  30669  mdsymlem8  30673  ordtconnlem1  31776  cvmliftlem15  33160  fvineqsneq  35510  lshpsmreu  37050  islpln5  37476  islvol5  37520  paddcom  37754  mapdrvallem2  39586  hdmapglem7a  39868  fsuppind  40202  fourierdlem42  43580  2rexsb  44480  2rexrsb  44481  pgrpgt2nabl  45590  islindeps2  45712  isldepslvec2  45714