Theorem rexcom 3294

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

Syntax hints:  ¬ wn 3   ↔ wb 209  ∀wral 3079  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-11 2194

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-ral 3080  df-rex 3090

This theorem is referenced by:  rexcom13  3298  2reurex  3726  2reu1  3853  2reu4lem  4480  iuncom  4960  xpiundi  5723  brdom7disj  10503  addcompr  10994  mulcompr  10996  qmulz  12966  elpq  12990  caubnd2  15399  ello1mpt2  15563  o1lo1  15578  lo1add  15668  lo1mul  15669  rlimno1  15695  sqrt2irr  16295  bezoutlem2  16588  bezoutlem4  16590  pythagtriplem19  16883  lsmcom2  19716  efgrelexlemb  19811  lsmcomx  19917  pgpfac1lem2  20138  pgpfac1lem4  20141  regsep2  23494  ordthaus  23502  tgcmp  23519  txcmplem1  23759  xkococnlem  23777  regr1lem2  23858  dyadmax  25718  coeeu  26343  ostth  27761  mulscom  28290  znegscl  28543  z12negscl  28629  z12sge0  28634  axpasch  29200  axeuclidlem  29221  usgr2pth0  30023  elwwlks2  30227  elwspths2spth  30228  shscom  31580  mdsymlem4  32667  mdsymlem8  32671  ordtconnlem1  34231  onvf1odlem1  35458  cvmliftlem15  35661  fvineqsneq  37918  lshpsmreu  39745  islpln5  40171  islvol5  40215  paddcom  40449  mapdrvallem2  42281  hdmapglem7a  42563  remexz  42733  hashnexinjle  42758  fimgmcyclem  43163  fsuppind  43184  fourierdlem42  46721  2rexsb  47693  2rexrsb  47694  pgrpgt2nabl  48997  islindeps2  49114  isldepslvec2  49116