Theorem rexcom 3277

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-11 2146

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

This theorem is referenced by:  rexcom13  3283  2reurex  3752  2reu1  3887  2reu4lem  4527  iuncom  5004  xpiundi  5748  brdom7disj  10556  addcompr  11046  mulcompr  11048  qmulz  12968  elpq  12992  caubnd2  15340  ello1mpt2  15502  o1lo1  15517  lo1add  15607  lo1mul  15608  rlimno1  15636  sqrt2irr  16229  bezoutlem2  16519  bezoutlem4  16521  pythagtriplem19  16805  lsmcom2  19622  efgrelexlemb  19717  lsmcomx  19823  pgpfac1lem2  20044  pgpfac1lem4  20047  regsep2  23324  ordthaus  23332  tgcmp  23349  txcmplem1  23589  xkococnlem  23607  regr1lem2  23688  dyadmax  25571  coeeu  26204  ostth  27617  mulscom  28089  znegscl  28289  axpasch  28824  axeuclidlem  28845  usgr2pth0  29651  elwwlks2  29849  elwspths2spth  29850  shscom  31201  mdsymlem4  32288  mdsymlem8  32292  ordtconnlem1  33656  cvmliftlem15  35039  fvineqsneq  37022  lshpsmreu  38711  islpln5  39138  islvol5  39182  paddcom  39416  mapdrvallem2  41248  hdmapglem7a  41530  remexz  41707  hashnexinjle  41732  fsuppind  41958  fourierdlem42  45675  2rexsb  46619  2rexrsb  46620  pgrpgt2nabl  47616  islindeps2  47737  isldepslvec2  47739