Theorem rexcom 3291

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 3290	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ¬ 𝜑)
2		ralnex2 3142	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
3		ralnex2 3142	. . 3 ⊢ (∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)
4	1, 2, 3	3bitr3i 304	. 2 ⊢ (¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ¬ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)
5	4	con4bii 324	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)

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

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 2194

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

This theorem is used by:  rexcom13  3295  2reurex  3718  2reu1  3845  2reu4lem  4479  iuncom  4959  xpiundi  5726  brdom7disj  10534  addcompr  11030  mulcompr  11032  qmulz  13000  elpq  13025  caubnd2  15445  ello1mpt2  15609  o1lo1  15624  lo1add  15714  lo1mul  15715  rlimno1  15741  sqrt2irr  16337  bezoutlem2  16630  bezoutlem4  16632  pythagtriplem19  16925  lsmcom2  19782  efgrelexlemb  19877  lsmcomx  19983  pgpfac1lem2  20204  pgpfac1lem4  20207  regsep2  23601  ordthaus  23609  tgcmp  23626  txcmplem1  23867  xkococnlem  23885  regr1lem2  23966  dyadmax  25826  coeeu  26451  ostth  27875  mulscom  28404  znegscl  28657  z12negscl  28743  z12sge0  28748  axpasch  29398  axeuclidlem  29419  usgr2pth0  30230  elwwlks2  30437  elwspths2spth  30438  shscom  31800  mdsymlem4  32887  mdsymlem8  32891  ordtconnlem1  34434  onvf1odlem1  35700  cvmliftlem15  35877  fvineqsneq  38166  lshpsmreu  39982  islpln5  40408  islvol5  40452  paddcom  40686  mapdrvallem2  42518  hdmapglem7a  42800  remexz  42970  hashnexinjle  42995  fimgmcyclem  43415  fsuppind  43436  fourierdlem42  46977  2rexsb  47989  2rexrsb  47990  pgrpgt2nabl  49296  islindeps2  49413  isldepslvec2  49415