Theorem rexcom 3266

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wral 3051  ∃wrex 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-11 2163

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-ral 3052  df-rex 3062

This theorem is referenced by:  rexcom13  3270  2reurex  3706  2reu1  3835  2reu4lem  4463  iuncom  4941  xpiundi  5702  brdom7disj  10453  addcompr  10944  mulcompr  10946  qmulz  12901  elpq  12925  caubnd2  15320  ello1mpt2  15484  o1lo1  15499  lo1add  15589  lo1mul  15590  rlimno1  15616  sqrt2irr  16216  bezoutlem2  16509  bezoutlem4  16511  pythagtriplem19  16804  lsmcom2  19630  efgrelexlemb  19725  lsmcomx  19831  pgpfac1lem2  20052  pgpfac1lem4  20055  regsep2  23341  ordthaus  23349  tgcmp  23366  txcmplem1  23606  xkococnlem  23624  regr1lem2  23705  dyadmax  25565  coeeu  26190  ostth  27602  mulscom  28131  znegscl  28384  z12negscl  28470  z12sge0  28475  axpasch  29010  axeuclidlem  29031  usgr2pth0  29833  elwwlks2  30037  elwspths2spth  30038  shscom  31390  mdsymlem4  32477  mdsymlem8  32481  ordtconnlem1  34068  onvf1odlem1  35285  cvmliftlem15  35480  fvineqsneq  37728  lshpsmreu  39555  islpln5  39981  islvol5  40025  paddcom  40259  mapdrvallem2  42091  hdmapglem7a  42373  remexz  42543  hashnexinjle  42568  fimgmcyclem  42978  fsuppind  43023  fourierdlem42  46577  2rexsb  47549  2rexrsb  47550  pgrpgt2nabl  48842  islindeps2  48959  isldepslvec2  48961