Theorem rexcom 3292

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

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

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 3078  df-rex 3088

This theorem is used by:  rexcom13  3296  2reurex  3718  2reu1  3845  2reu4lem  4479  iuncom  4959  xpiundi  5722  brdom7disj  10591  addcompr  11087  mulcompr  11089  qmulz  13059  elpq  13084  caubnd2  15505  ello1mpt2  15669  o1lo1  15684  lo1add  15774  lo1mul  15775  rlimno1  15801  sqrt2irr  16397  bezoutlem2  16693  bezoutlem4  16695  pythagtriplem19  16991  lsmcom2  19849  efgrelexlemb  19944  lsmcomx  20050  pgpfac1lem2  20271  pgpfac1lem4  20274  regsep2  23674  ordthaus  23682  tgcmp  23699  txcmplem1  23940  xkococnlem  23958  regr1lem2  24039  dyadmax  25899  coeeu  26524  ostth  27948  mulscom  28507  znegscl  28760  z12negscl  28846  z12sge0  28851  axpasch  29501  axeuclidlem  29522  usgr2pth0  30333  elwwlks2  30540  elwspths2spth  30541  shscom  31903  mdsymlem4  32990  mdsymlem8  32994  ordtconnlem1  34538  onvf1odlem1  35855  cvmliftlem15  36032  fvineqsneq  38303  lshpsmreu  40134  islpln5  40560  islvol5  40604  paddcom  40838  mapdrvallem2  42670  hdmapglem7a  42952  remexz  43122  hashnexinjle  43147  fimgmcyclem  43559  fsuppind  43580  fourierdlem42  47103  2rexsb  48115  2rexrsb  48116  pgrpgt2nabl  49422  islindeps2  49539  isldepslvec2  49541