Theorem rexcom 3266

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 3265	. . 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 3044  ∃wrex 3053

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 1910  ax-11 2158

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3045  df-rex 3054

This theorem is referenced by:  rexcom13  3271  2reurex  3731  2reu1  3860  2reu4lem  4485  iuncom  4963  xpiundi  5709  brdom7disj  10484  addcompr  10974  mulcompr  10976  qmulz  12910  elpq  12934  caubnd2  15324  ello1mpt2  15488  o1lo1  15503  lo1add  15593  lo1mul  15594  rlimno1  15620  sqrt2irr  16217  bezoutlem2  16510  bezoutlem4  16512  pythagtriplem19  16804  lsmcom2  19585  efgrelexlemb  19680  lsmcomx  19786  pgpfac1lem2  20007  pgpfac1lem4  20010  regsep2  23263  ordthaus  23271  tgcmp  23288  txcmplem1  23528  xkococnlem  23546  regr1lem2  23627  dyadmax  25499  coeeu  26130  ostth  27550  mulscom  28042  znegscl  28280  zs12negscl  28340  zs12ge0  28342  axpasch  28868  axeuclidlem  28889  usgr2pth0  29695  elwwlks2  29896  elwspths2spth  29897  shscom  31248  mdsymlem4  32335  mdsymlem8  32339  ordtconnlem1  33914  onvf1odlem1  35090  cvmliftlem15  35285  fvineqsneq  37400  lshpsmreu  39102  islpln5  39529  islvol5  39573  paddcom  39807  mapdrvallem2  41639  hdmapglem7a  41921  remexz  42092  hashnexinjle  42117  fimgmcyclem  42521  fsuppind  42578  fourierdlem42  46147  2rexsb  47102  2rexrsb  47103  pgrpgt2nabl  48354  islindeps2  48472  isldepslvec2  48474