Theorem rexcom 3355

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 3144	. . 3 ⊢ (∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜑))
2	1	rexbii 3247	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜑))
3		rexcom4 3249	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜑) ↔ ∃𝑦∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 ∧ 𝜑))
4		r19.42v 3350	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 ∧ 𝜑) ↔ (𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑))
5	4	exbii 1844	. . 3 ⊢ (∃𝑦∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 ∧ 𝜑) ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑))
6		df-rex 3144	. . 3 ⊢ (∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑))
7	5, 6	bitr4i 280	. 2 ⊢ (∃𝑦∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 ∧ 𝜑) ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)
8	2, 3, 7	3bitri 299	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   ↔ wb 208   ∧ wa 398  ∃wex 1776   ∈ wcel 2110  ∃wrex 3139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-11 2157

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-rex 3144

This theorem is referenced by:  rexcom13  3360  rexcom4OLD  3526  2reurex  3749  2reu1  3880  2reu4lem  4464  iuncom  4918  xpiundi  5616  brdom7disj  9947  addcompr  10437  mulcompr  10439  qmulz  12345  elpq  12368  caubnd2  14711  ello1mpt2  14873  o1lo1  14888  lo1add  14977  lo1mul  14978  rlimno1  15004  sqrt2irr  15596  bezoutlem2  15882  bezoutlem4  15884  pythagtriplem19  16164  lsmcom2  18774  efgrelexlemb  18870  lsmcomx  18970  pgpfac1lem2  19191  pgpfac1lem4  19194  regsep2  21978  ordthaus  21986  tgcmp  22003  txcmplem1  22243  xkococnlem  22261  regr1lem2  22342  dyadmax  24193  coeeu  24809  ostth  26209  axpasch  26721  axeuclidlem  26742  usgr2pth0  27540  elwwlks2  27739  elwspths2spth  27740  shscom  29090  mdsymlem4  30177  mdsymlem8  30181  ordtconnlem1  31162  cvmliftlem15  32540  fvineqsneq  34687  lshpsmreu  36239  islpln5  36665  islvol5  36709  paddcom  36943  mapdrvallem2  38775  hdmapglem7a  39057  fourierdlem42  42428  2rexsb  43293  2rexrsb  43294  pgrpgt2nabl  44408  islindeps2  44532  isldepslvec2  44534