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  3720  2reu1  3849  2reu4lem  4478  iuncom  4956  xpiundi  5703  brdom7disj  10453  addcompr  10944  mulcompr  10946  qmulz  12876  elpq  12900  caubnd2  15293  ello1mpt2  15457  o1lo1  15472  lo1add  15562  lo1mul  15563  rlimno1  15589  sqrt2irr  16186  bezoutlem2  16479  bezoutlem4  16481  pythagtriplem19  16773  lsmcom2  19596  efgrelexlemb  19691  lsmcomx  19797  pgpfac1lem2  20018  pgpfac1lem4  20021  regsep2  23332  ordthaus  23340  tgcmp  23357  txcmplem1  23597  xkococnlem  23615  regr1lem2  23696  dyadmax  25567  coeeu  26198  ostth  27618  mulscom  28147  znegscl  28400  z12negscl  28486  z12sge0  28491  axpasch  29026  axeuclidlem  29047  usgr2pth0  29850  elwwlks2  30054  elwspths2spth  30055  shscom  31406  mdsymlem4  32493  mdsymlem8  32497  ordtconnlem1  34101  onvf1odlem1  35316  cvmliftlem15  35511  fvineqsneq  37661  lshpsmreu  39479  islpln5  39905  islvol5  39949  paddcom  40183  mapdrvallem2  42015  hdmapglem7a  42297  remexz  42468  hashnexinjle  42493  fimgmcyclem  42897  fsuppind  42942  fourierdlem42  46501  2rexsb  47455  2rexrsb  47456  pgrpgt2nabl  48720  islindeps2  48837  isldepslvec2  48839