Theorem rexcom 3265

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wral 3051  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-11 2162

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-ral 3052  df-rex 3061

This theorem is referenced by:  rexcom13  3269  2reurex  3718  2reu1  3847  2reu4lem  4476  iuncom  4954  xpiundi  5695  brdom7disj  10441  addcompr  10932  mulcompr  10934  qmulz  12864  elpq  12888  caubnd2  15281  ello1mpt2  15445  o1lo1  15460  lo1add  15550  lo1mul  15551  rlimno1  15577  sqrt2irr  16174  bezoutlem2  16467  bezoutlem4  16469  pythagtriplem19  16761  lsmcom2  19584  efgrelexlemb  19679  lsmcomx  19785  pgpfac1lem2  20006  pgpfac1lem4  20009  regsep2  23320  ordthaus  23328  tgcmp  23345  txcmplem1  23585  xkococnlem  23603  regr1lem2  23684  dyadmax  25555  coeeu  26186  ostth  27606  mulscom  28135  znegscl  28388  z12negscl  28474  z12sge0  28479  axpasch  29014  axeuclidlem  29035  usgr2pth0  29838  elwwlks2  30042  elwspths2spth  30043  shscom  31394  mdsymlem4  32481  mdsymlem8  32485  ordtconnlem1  34081  onvf1odlem1  35297  cvmliftlem15  35492  fvineqsneq  37613  lshpsmreu  39365  islpln5  39791  islvol5  39835  paddcom  40069  mapdrvallem2  41901  hdmapglem7a  42183  remexz  42354  hashnexinjle  42379  fimgmcyclem  42784  fsuppind  42829  fourierdlem42  46389  2rexsb  47343  2rexrsb  47344  pgrpgt2nabl  48608  islindeps2  48725  isldepslvec2  48727