Theorem rexcom 3262

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wral 3048  ∃wrex 3057

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 2162

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

This theorem is referenced by:  rexcom13  3266  2reurex  3715  2reu1  3844  2reu4lem  4471  iuncom  4949  xpiundi  5690  brdom7disj  10429  addcompr  10919  mulcompr  10921  qmulz  12851  elpq  12875  caubnd2  15267  ello1mpt2  15431  o1lo1  15446  lo1add  15536  lo1mul  15537  rlimno1  15563  sqrt2irr  16160  bezoutlem2  16453  bezoutlem4  16455  pythagtriplem19  16747  lsmcom2  19569  efgrelexlemb  19664  lsmcomx  19770  pgpfac1lem2  19991  pgpfac1lem4  19994  regsep2  23292  ordthaus  23300  tgcmp  23317  txcmplem1  23557  xkococnlem  23575  regr1lem2  23656  dyadmax  25527  coeeu  26158  ostth  27578  mulscom  28079  znegscl  28317  zs12negscl  28389  zs12ge0  28394  axpasch  28921  axeuclidlem  28942  usgr2pth0  29745  elwwlks2  29949  elwspths2spth  29950  shscom  31301  mdsymlem4  32388  mdsymlem8  32392  ordtconnlem1  33958  onvf1odlem1  35168  cvmliftlem15  35363  fvineqsneq  37477  lshpsmreu  39228  islpln5  39654  islvol5  39698  paddcom  39932  mapdrvallem2  41764  hdmapglem7a  42046  remexz  42217  hashnexinjle  42242  fimgmcyclem  42651  fsuppind  42708  fourierdlem42  46271  2rexsb  47225  2rexrsb  47226  pgrpgt2nabl  48490  islindeps2  48608  isldepslvec2  48610