Theorem rexcom 3261

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wral 3047  ∃wrex 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-11 2160

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-ral 3048  df-rex 3057

This theorem is referenced by:  rexcom13  3265  2reurex  3719  2reu1  3848  2reu4lem  4472  iuncom  4949  xpiundi  5687  brdom7disj  10419  addcompr  10909  mulcompr  10911  qmulz  12846  elpq  12870  caubnd2  15262  ello1mpt2  15426  o1lo1  15441  lo1add  15531  lo1mul  15532  rlimno1  15558  sqrt2irr  16155  bezoutlem2  16448  bezoutlem4  16450  pythagtriplem19  16742  lsmcom2  19565  efgrelexlemb  19660  lsmcomx  19766  pgpfac1lem2  19987  pgpfac1lem4  19990  regsep2  23289  ordthaus  23297  tgcmp  23314  txcmplem1  23554  xkococnlem  23572  regr1lem2  23653  dyadmax  25524  coeeu  26155  ostth  27575  mulscom  28076  znegscl  28314  zs12negscl  28386  zs12ge0  28391  axpasch  28917  axeuclidlem  28938  usgr2pth0  29741  elwwlks2  29942  elwspths2spth  29943  shscom  31294  mdsymlem4  32381  mdsymlem8  32385  ordtconnlem1  33932  onvf1odlem1  35135  cvmliftlem15  35330  fvineqsneq  37445  lshpsmreu  39147  islpln5  39573  islvol5  39617  paddcom  39851  mapdrvallem2  41683  hdmapglem7a  41965  remexz  42136  hashnexinjle  42161  fimgmcyclem  42565  fsuppind  42622  fourierdlem42  46186  2rexsb  47131  2rexrsb  47132  pgrpgt2nabl  48396  islindeps2  48514  isldepslvec2  48516