Theorem rexcom 3269

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

Syntax hints:  ¬ wn 3   ↔ wb 207  ∀wral 3054  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-11 2168

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-ral 3055  df-rex 3065

This theorem is referenced by:  rexcom13  3273  2reurex  3708  2reu1  3836  2reu4lem  4458  iuncom  4936  xpiundi  5696  brdom7disj  10451  addcompr  10942  mulcompr  10944  qmulz  12899  elpq  12923  caubnd2  15318  ello1mpt2  15482  o1lo1  15497  lo1add  15587  lo1mul  15588  rlimno1  15614  sqrt2irr  16214  bezoutlem2  16507  bezoutlem4  16509  pythagtriplem19  16802  lsmcom2  19628  efgrelexlemb  19723  lsmcomx  19829  pgpfac1lem2  20050  pgpfac1lem4  20053  regsep2  23366  ordthaus  23374  tgcmp  23391  txcmplem1  23631  xkococnlem  23649  regr1lem2  23730  dyadmax  25590  coeeu  26215  ostth  27627  mulscom  28156  znegscl  28409  z12negscl  28495  z12sge0  28500  axpasch  29035  axeuclidlem  29056  usgr2pth0  29858  elwwlks2  30062  elwspths2spth  30063  shscom  31415  mdsymlem4  32502  mdsymlem8  32506  ordtconnlem1  34115  onvf1odlem1  35338  cvmliftlem15  35533  fvineqsneq  37781  lshpsmreu  39608  islpln5  40034  islvol5  40078  paddcom  40312  mapdrvallem2  42144  hdmapglem7a  42426  remexz  42596  hashnexinjle  42621  fimgmcyclem  43026  fsuppind  43047  fourierdlem42  46599  2rexsb  47571  2rexrsb  47572  pgrpgt2nabl  48864  islindeps2  48981  isldepslvec2  48983