Theorem rexcom 3234

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

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wral 3064  ∃wrex 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-11 2154

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-ral 3069  df-rex 3070

This theorem is referenced by:  rexcom13  3287  2reurex  3695  2reu1  3830  2reu4lem  4456  iuncom  4931  xpiundi  5657  brdom7disj  10287  addcompr  10777  mulcompr  10779  qmulz  12691  elpq  12715  caubnd2  15069  ello1mpt2  15231  o1lo1  15246  lo1add  15336  lo1mul  15337  rlimno1  15365  sqrt2irr  15958  bezoutlem2  16248  bezoutlem4  16250  pythagtriplem19  16534  lsmcom2  19260  efgrelexlemb  19356  lsmcomx  19457  pgpfac1lem2  19678  pgpfac1lem4  19681  regsep2  22527  ordthaus  22535  tgcmp  22552  txcmplem1  22792  xkococnlem  22810  regr1lem2  22891  dyadmax  24762  coeeu  25386  ostth  26787  axpasch  27309  axeuclidlem  27330  usgr2pth0  28133  elwwlks2  28331  elwspths2spth  28332  shscom  29681  mdsymlem4  30768  mdsymlem8  30772  ordtconnlem1  31874  cvmliftlem15  33260  fvineqsneq  35583  lshpsmreu  37123  islpln5  37549  islvol5  37593  paddcom  37827  mapdrvallem2  39659  hdmapglem7a  39941  fsuppind  40279  fourierdlem42  43690  2rexsb  44593  2rexrsb  44594  pgrpgt2nabl  45702  islindeps2  45824  isldepslvec2  45826