Theorem rexcom 3285

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 3284	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ¬ 𝜑)
2		ralnex2 3131	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
3		ralnex2 3131	. . 3 ⊢ (∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)
4	1, 2, 3	3bitr3i 300	. 2 ⊢ (¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ¬ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)
5	4	con4bii 320	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wral 3059  ∃wrex 3068

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 1911  ax-11 2152

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-ral 3060  df-rex 3069

This theorem is referenced by:  rexcom13  3291  2reurex  3755  2reu1  3890  2reu4lem  4524  iuncom  5003  xpiundi  5745  brdom7disj  10528  addcompr  11018  mulcompr  11020  qmulz  12939  elpq  12963  caubnd2  15308  ello1mpt2  15470  o1lo1  15485  lo1add  15575  lo1mul  15576  rlimno1  15604  sqrt2irr  16196  bezoutlem2  16486  bezoutlem4  16488  pythagtriplem19  16770  lsmcom2  19564  efgrelexlemb  19659  lsmcomx  19765  pgpfac1lem2  19986  pgpfac1lem4  19989  regsep2  23100  ordthaus  23108  tgcmp  23125  txcmplem1  23365  xkococnlem  23383  regr1lem2  23464  dyadmax  25347  coeeu  25974  ostth  27378  mulscom  27834  axpasch  28466  axeuclidlem  28487  usgr2pth0  29289  elwwlks2  29487  elwspths2spth  29488  shscom  30839  mdsymlem4  31926  mdsymlem8  31930  ordtconnlem1  33202  cvmliftlem15  34587  fvineqsneq  36596  lshpsmreu  38282  islpln5  38709  islvol5  38753  paddcom  38987  mapdrvallem2  40819  hdmapglem7a  41101  fsuppind  41464  fourierdlem42  45163  2rexsb  46107  2rexrsb  46108  pgrpgt2nabl  47130  islindeps2  47251  isldepslvec2  47253