Theorem rexcom 3267

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wral 3052  ∃wrex 3062

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 3053  df-rex 3063

This theorem is referenced by:  rexcom13  3271  2reurex  3707  2reu1  3836  2reu4lem  4464  iuncom  4942  xpiundi  5695  brdom7disj  10444  addcompr  10935  mulcompr  10937  qmulz  12892  elpq  12916  caubnd2  15311  ello1mpt2  15475  o1lo1  15490  lo1add  15580  lo1mul  15581  rlimno1  15607  sqrt2irr  16207  bezoutlem2  16500  bezoutlem4  16502  pythagtriplem19  16795  lsmcom2  19621  efgrelexlemb  19716  lsmcomx  19822  pgpfac1lem2  20043  pgpfac1lem4  20046  regsep2  23351  ordthaus  23359  tgcmp  23376  txcmplem1  23616  xkococnlem  23634  regr1lem2  23715  dyadmax  25575  coeeu  26200  ostth  27616  mulscom  28145  znegscl  28398  z12negscl  28484  z12sge0  28489  axpasch  29024  axeuclidlem  29045  usgr2pth0  29848  elwwlks2  30052  elwspths2spth  30053  shscom  31405  mdsymlem4  32492  mdsymlem8  32496  ordtconnlem1  34084  onvf1odlem1  35301  cvmliftlem15  35496  fvineqsneq  37742  lshpsmreu  39569  islpln5  39995  islvol5  40039  paddcom  40273  mapdrvallem2  42105  hdmapglem7a  42387  remexz  42557  hashnexinjle  42582  fimgmcyclem  42992  fsuppind  43037  fourierdlem42  46595  2rexsb  47561  2rexrsb  47562  pgrpgt2nabl  48854  islindeps2  48971  isldepslvec2  48973