Theorem rexcom 3358

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

Syntax hints:   ↔ wb 208   ∧ wa 398  ∃wex 1779   ∈ wcel 2113  ∃wrex 3142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-11 2160

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-rex 3147

This theorem is referenced by:  rexcom13  3363  rexcom4OLD  3529  2reurex  3753  2reu1  3884  2reu4lem  4468  iuncom  4929  xpiundi  5625  brdom7disj  9956  addcompr  10446  mulcompr  10448  qmulz  12354  elpq  12377  caubnd2  14720  ello1mpt2  14882  o1lo1  14897  lo1add  14986  lo1mul  14987  rlimno1  15013  sqrt2irr  15605  bezoutlem2  15891  bezoutlem4  15893  pythagtriplem19  16173  lsmcom2  18783  efgrelexlemb  18879  lsmcomx  18979  pgpfac1lem2  19200  pgpfac1lem4  19203  regsep2  21987  ordthaus  21995  tgcmp  22012  txcmplem1  22252  xkococnlem  22270  regr1lem2  22351  dyadmax  24202  coeeu  24818  ostth  26218  axpasch  26730  axeuclidlem  26751  usgr2pth0  27549  elwwlks2  27748  elwspths2spth  27749  shscom  29099  mdsymlem4  30186  mdsymlem8  30190  ordtconnlem1  31171  cvmliftlem15  32549  fvineqsneq  34697  lshpsmreu  36249  islpln5  36675  islvol5  36719  paddcom  36953  mapdrvallem2  38785  hdmapglem7a  39067  fourierdlem42  42441  2rexsb  43306  2rexrsb  43307  pgrpgt2nabl  44421  islindeps2  44545  isldepslvec2  44547