Theorem rexcom 3296

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 3295	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ¬ 𝜑)
2		ralnex2 3139	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
3		ralnex2 3139	. . 3 ⊢ (∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)
4	1, 2, 3	3bitr3i 301	. 2 ⊢ (¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ¬ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)
5	4	con4bii 321	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wral 3067  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-11 2158

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-ral 3068  df-rex 3077

This theorem is referenced by:  rexcom13  3302  2reurex  3782  2reu1  3919  2reu4lem  4545  iuncom  5022  xpiundi  5770  brdom7disj  10600  addcompr  11090  mulcompr  11092  qmulz  13016  elpq  13040  caubnd2  15406  ello1mpt2  15568  o1lo1  15583  lo1add  15673  lo1mul  15674  rlimno1  15702  sqrt2irr  16297  bezoutlem2  16587  bezoutlem4  16589  pythagtriplem19  16880  lsmcom2  19697  efgrelexlemb  19792  lsmcomx  19898  pgpfac1lem2  20119  pgpfac1lem4  20122  regsep2  23405  ordthaus  23413  tgcmp  23430  txcmplem1  23670  xkococnlem  23688  regr1lem2  23769  dyadmax  25652  coeeu  26284  ostth  27701  mulscom  28183  znegscl  28396  axpasch  28974  axeuclidlem  28995  usgr2pth0  29801  elwwlks2  29999  elwspths2spth  30000  shscom  31351  mdsymlem4  32438  mdsymlem8  32442  ordtconnlem1  33870  cvmliftlem15  35266  fvineqsneq  37378  lshpsmreu  39065  islpln5  39492  islvol5  39536  paddcom  39770  mapdrvallem2  41602  hdmapglem7a  41884  remexz  42061  hashnexinjle  42086  fimgmcyclem  42488  fsuppind  42545  fourierdlem42  46070  2rexsb  47016  2rexrsb  47017  pgrpgt2nabl  48091  islindeps2  48212  isldepslvec2  48214