Theorem rexcom 3258

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 3257	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ¬ 𝜑)
2		ralnex2 3109	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
3		ralnex2 3109	. . 3 ⊢ (∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)
4	1, 2, 3	3bitr3i 301	. 2 ⊢ (¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ¬ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)
5	4	con4bii 321	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wral 3044  ∃wrex 3053

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 2158

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3045  df-rex 3054

This theorem is referenced by:  rexcom13  3263  2reurex  3722  2reu1  3851  2reu4lem  4475  iuncom  4952  xpiundi  5694  brdom7disj  10444  addcompr  10934  mulcompr  10936  qmulz  12870  elpq  12894  caubnd2  15283  ello1mpt2  15447  o1lo1  15462  lo1add  15552  lo1mul  15553  rlimno1  15579  sqrt2irr  16176  bezoutlem2  16469  bezoutlem4  16471  pythagtriplem19  16763  lsmcom2  19552  efgrelexlemb  19647  lsmcomx  19753  pgpfac1lem2  19974  pgpfac1lem4  19977  regsep2  23279  ordthaus  23287  tgcmp  23304  txcmplem1  23544  xkococnlem  23562  regr1lem2  23643  dyadmax  25515  coeeu  26146  ostth  27566  mulscom  28065  znegscl  28303  zs12negscl  28373  zs12ge0  28378  axpasch  28904  axeuclidlem  28925  usgr2pth0  29728  elwwlks2  29929  elwspths2spth  29930  shscom  31281  mdsymlem4  32368  mdsymlem8  32372  ordtconnlem1  33890  onvf1odlem1  35075  cvmliftlem15  35270  fvineqsneq  37385  lshpsmreu  39087  islpln5  39514  islvol5  39558  paddcom  39792  mapdrvallem2  41624  hdmapglem7a  41906  remexz  42077  hashnexinjle  42102  fimgmcyclem  42506  fsuppind  42563  fourierdlem42  46131  2rexsb  47086  2rexrsb  47087  pgrpgt2nabl  48351  islindeps2  48469  isldepslvec2  48471