Theorem rexcom 3271

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wral 3051  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-11 2157

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3052  df-rex 3061

This theorem is referenced by:  rexcom13  3277  2reurex  3743  2reu1  3872  2reu4lem  4497  iuncom  4975  xpiundi  5725  brdom7disj  10545  addcompr  11035  mulcompr  11037  qmulz  12967  elpq  12991  caubnd2  15376  ello1mpt2  15538  o1lo1  15553  lo1add  15643  lo1mul  15644  rlimno1  15670  sqrt2irr  16267  bezoutlem2  16559  bezoutlem4  16561  pythagtriplem19  16853  lsmcom2  19636  efgrelexlemb  19731  lsmcomx  19837  pgpfac1lem2  20058  pgpfac1lem4  20061  regsep2  23314  ordthaus  23322  tgcmp  23339  txcmplem1  23579  xkococnlem  23597  regr1lem2  23678  dyadmax  25551  coeeu  26182  ostth  27602  mulscom  28094  znegscl  28332  zs12negscl  28392  zs12ge0  28394  axpasch  28920  axeuclidlem  28941  usgr2pth0  29747  elwwlks2  29948  elwspths2spth  29949  shscom  31300  mdsymlem4  32387  mdsymlem8  32391  ordtconnlem1  33955  cvmliftlem15  35320  fvineqsneq  37430  lshpsmreu  39127  islpln5  39554  islvol5  39598  paddcom  39832  mapdrvallem2  41664  hdmapglem7a  41946  remexz  42117  hashnexinjle  42142  fimgmcyclem  42556  fsuppind  42613  fourierdlem42  46178  2rexsb  47130  2rexrsb  47131  pgrpgt2nabl  48341  islindeps2  48459  isldepslvec2  48461