Theorem rexcom 3291

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 3290	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ¬ 𝜑)
2		ralnex2 3142	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
3		ralnex2 3142	. . 3 ⊢ (∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)
4	1, 2, 3	3bitr3i 304	. 2 ⊢ (¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ¬ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)
5	4	con4bii 324	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209  ∀wral 3076  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-11 2193

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-ral 3077  df-rex 3087

This theorem is used by:  rexcom13  3295  2reurex  3717  2reu1  3844  2reu4lem  4478  iuncom  4958  xpiundi  5721  brdom7disj  10613  addcompr  11109  mulcompr  11111  qmulz  13081  elpq  13106  caubnd2  15530  ello1mpt2  15694  o1lo1  15709  lo1add  15799  lo1mul  15800  rlimno1  15826  sqrt2irr  16422  bezoutlem2  16718  bezoutlem4  16720  pythagtriplem19  17016  lsmcom2  19874  efgrelexlemb  19969  lsmcomx  20075  pgpfac1lem2  20296  pgpfac1lem4  20299  regsep2  23699  ordthaus  23707  tgcmp  23724  txcmplem1  23965  xkococnlem  23983  regr1lem2  24064  dyadmax  25924  coeeu  26549  ostth  27971  mulscom  28530  znegscl  28783  z12negscl  28869  z12sge0  28874  axpasch  29524  axeuclidlem  29545  usgr2pth0  30356  elwwlks2  30563  elwspths2spth  30564  shscom  31926  mdsymlem4  33013  mdsymlem8  33017  ordtconnlem1  34602  onvf1odlem1  35950  cvmliftlem15  36149  fvineqsneq  38428  lshpsmreu  40259  islpln5  40685  islvol5  40729  paddcom  40963  mapdrvallem2  42795  hdmapglem7a  43077  remexz  43247  hashnexinjle  43272  fimgmcyclem  43690  fsuppind  43711  fourierdlem42  47252  2rexsb  48264  2rexrsb  48265  pgrpgt2nabl  49571  islindeps2  49688  isldepslvec2  49690