Theorem rexcom 3290

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 3289	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ¬ 𝜑)
2		ralnex2 3141	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
3		ralnex2 3141	. . 3 ⊢ (∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)
4	1, 2, 3	3bitr3i 303	. 2 ⊢ (¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ¬ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)
5	4	con4bii 323	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 208  ∀wral 3075  ∃wrex 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-11 2190

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-ral 3076  df-rex 3086

This theorem is referenced by:  rexcom13  3294  2reurex  3722  2reu1  3850  2reu4lem  4476  iuncom  4956  xpiundi  5716  brdom7disj  10485  addcompr  10976  mulcompr  10978  qmulz  12949  elpq  12973  caubnd2  15368  ello1mpt2  15532  o1lo1  15547  lo1add  15637  lo1mul  15638  rlimno1  15664  sqrt2irr  16264  bezoutlem2  16557  bezoutlem4  16559  pythagtriplem19  16852  lsmcom2  19678  efgrelexlemb  19773  lsmcomx  19879  pgpfac1lem2  20100  pgpfac1lem4  20103  regsep2  23416  ordthaus  23424  tgcmp  23441  txcmplem1  23681  xkococnlem  23699  regr1lem2  23780  dyadmax  25640  coeeu  26265  ostth  27680  mulscom  28209  znegscl  28462  z12negscl  28548  z12sge0  28553  axpasch  29088  axeuclidlem  29109  usgr2pth0  29911  elwwlks2  30115  elwspths2spth  30116  shscom  31468  mdsymlem4  32555  mdsymlem8  32559  ordtconnlem1  34182  onvf1odlem1  35410  cvmliftlem15  35612  fvineqsneq  37870  lshpsmreu  39697  islpln5  40123  islvol5  40167  paddcom  40401  mapdrvallem2  42233  hdmapglem7a  42515  remexz  42685  hashnexinjle  42710  fimgmcyclem  43115  fsuppind  43136  fourierdlem42  46687  2rexsb  47659  2rexrsb  47660  pgrpgt2nabl  48952  islindeps2  49069  isldepslvec2  49071