Theorem rexcom 3293

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 3292	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ¬ 𝜑)
2		ralnex2 3144	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
3		ralnex2 3144	. . 3 ⊢ (∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)
4	1, 2, 3	3bitr3i 304	. 2 ⊢ (¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ¬ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)
5	4	con4bii 324	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209  ∀wral 3078  ∃wrex 3088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-11 2194

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3079  df-rex 3089

This theorem is used by:  rexcom13  3297  2reurex  3721  2reu1  3848  2reu4lem  4482  iuncom  4962  xpiundi  5730  brdom7disj  10538  addcompr  11034  mulcompr  11036  qmulz  13004  elpq  13029  caubnd2  15449  ello1mpt2  15613  o1lo1  15628  lo1add  15718  lo1mul  15719  rlimno1  15745  sqrt2irr  16343  bezoutlem2  16636  bezoutlem4  16638  pythagtriplem19  16931  lsmcom2  19788  efgrelexlemb  19883  lsmcomx  19989  pgpfac1lem2  20210  pgpfac1lem4  20213  regsep2  23607  ordthaus  23615  tgcmp  23632  txcmplem1  23873  xkococnlem  23891  regr1lem2  23972  dyadmax  25832  coeeu  26458  ostth  27883  mulscom  28412  znegscl  28665  z12negscl  28751  z12sge0  28756  axpasch  29406  axeuclidlem  29427  usgr2pth0  30238  elwwlks2  30445  elwspths2spth  30446  shscom  31808  mdsymlem4  32895  mdsymlem8  32899  ordtconnlem1  34442  onvf1odlem1  35708  cvmliftlem15  35885  fvineqsneq  38174  lshpsmreu  39990  islpln5  40416  islvol5  40460  paddcom  40694  mapdrvallem2  42526  hdmapglem7a  42808  remexz  42978  hashnexinjle  43003  fimgmcyclem  43423  fsuppind  43444  fourierdlem42  46985  2rexsb  47997  2rexrsb  47998  pgrpgt2nabl  49304  islindeps2  49421  isldepslvec2  49423