Theorem rexcom 3287

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 3286	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ¬ 𝜑)
2		ralnex2 3133	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
3		ralnex2 3133	. . 3 ⊢ (∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)
4	1, 2, 3	3bitr3i 300	. 2 ⊢ (¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ¬ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)
5	4	con4bii 320	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wral 3061  ∃wrex 3070

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 1913  ax-11 2154

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-ral 3062  df-rex 3071

This theorem is referenced by:  rexcom13  3293  2reurex  3756  2reu1  3891  2reu4lem  4525  iuncom  5004  xpiundi  5746  brdom7disj  10525  addcompr  11015  mulcompr  11017  qmulz  12934  elpq  12958  caubnd2  15303  ello1mpt2  15465  o1lo1  15480  lo1add  15570  lo1mul  15571  rlimno1  15599  sqrt2irr  16191  bezoutlem2  16481  bezoutlem4  16483  pythagtriplem19  16765  lsmcom2  19522  efgrelexlemb  19617  lsmcomx  19723  pgpfac1lem2  19944  pgpfac1lem4  19947  regsep2  22879  ordthaus  22887  tgcmp  22904  txcmplem1  23144  xkococnlem  23162  regr1lem2  23243  dyadmax  25114  coeeu  25738  ostth  27139  mulscom  27592  axpasch  28196  axeuclidlem  28217  usgr2pth0  29019  elwwlks2  29217  elwspths2spth  29218  shscom  30567  mdsymlem4  31654  mdsymlem8  31658  ordtconnlem1  32899  cvmliftlem15  34284  fvineqsneq  36288  lshpsmreu  37974  islpln5  38401  islvol5  38445  paddcom  38679  mapdrvallem2  40511  hdmapglem7a  40793  fsuppind  41164  fourierdlem42  44855  2rexsb  45799  2rexrsb  45800  pgrpgt2nabl  47032  islindeps2  47154  isldepslvec2  47156