Theorem rexcom 3297

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.) (Proof shortened by Wolf Lammen, 8-Dec-2024.)

Assertion

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

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

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

Proof of Theorem rexcom

Step	Hyp	Ref	Expression
1		ralcom 3296	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ¬ 𝜑)
2		ralnex2 3148	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
3		ralnex2 3148	. . 3 ⊢ (∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)
4	1, 2, 3	3bitr3i 304	. 2 ⊢ (¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ¬ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)
5	4	con4bii 324	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209  ∀wral 3082  ∃wrex 3092

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-11 2195

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3083  df-rex 3093

This theorem is used by:  rexcom13  3301  2reurex  3726  2reu1  3854  2reu4lem  4489  iuncom  4969  xpiundi  5737  brdom7disj  10533  addcompr  11024  mulcompr  11026  qmulz  12993  elpq  13017  caubnd2  15435  ello1mpt2  15599  o1lo1  15614  lo1add  15704  lo1mul  15705  rlimno1  15731  sqrt2irr  16330  bezoutlem2  16623  bezoutlem4  16625  pythagtriplem19  16918  lsmcom2  19756  efgrelexlemb  19851  lsmcomx  19957  pgpfac1lem2  20178  pgpfac1lem4  20181  regsep2  23570  ordthaus  23578  tgcmp  23595  txcmplem1  23835  xkococnlem  23853  regr1lem2  23934  dyadmax  25794  coeeu  26419  ostth  27840  mulscom  28369  znegscl  28622  z12negscl  28708  z12sge0  28713  axpasch  29328  axeuclidlem  29349  usgr2pth0  30151  elwwlks2  30355  elwspths2spth  30356  shscom  31708  mdsymlem4  32795  mdsymlem8  32799  ordtconnlem1  34345  onvf1odlem1  35610  cvmliftlem15  35810  fvineqsneq  38098  lshpsmreu  39923  islpln5  40349  islvol5  40393  paddcom  40627  mapdrvallem2  42459  hdmapglem7a  42741  remexz  42911  hashnexinjle  42936  fimgmcyclem  43341  fsuppind  43362  fourierdlem42  46903  2rexsb  47878  2rexrsb  47879  pgrpgt2nabl  49186  islindeps2  49303  isldepslvec2  49305