Theorem rexcom 3295

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-11 2197

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3081  df-rex 3091

This theorem is used by:  rexcom13  3299  2reurex  3721  2reu1  3849  2reu4lem  4482  iuncom  4962  xpiundi  5726  brdom7disj  10637  addcompr  11133  mulcompr  11135  qmulz  13105  elpq  13130  caubnd2  15554  ello1mpt2  15718  o1lo1  15733  lo1add  15823  lo1mul  15824  rlimno1  15850  sqrt2irr  16446  bezoutlem2  16742  bezoutlem4  16744  pythagtriplem19  17040  lsmcom2  19899  efgrelexlemb  19994  lsmcomx  20100  pgpfac1lem2  20321  pgpfac1lem4  20324  regsep2  23724  ordthaus  23732  tgcmp  23749  txcmplem1  23990  xkococnlem  24008  regr1lem2  24089  dyadmax  25949  coeeu  26574  ostth  27996  mulscom  28555  znegscl  28808  z12negscl  28894  z12sge0  28899  axpasch  29549  axeuclidlem  29570  usgr2pth0  30381  elwwlks2  30588  elwspths2spth  30589  shscom  31951  mdsymlem4  33038  mdsymlem8  33042  ordtconnlem1  34626  onvf1odlem1  36031  cvmliftlem15  36230  fvineqsneq  38527  lshpsmreu  40358  islpln5  40784  islvol5  40828  paddcom  41062  mapdrvallem2  42894  hdmapglem7a  43176  remexz  43346  hashnexinjle  43371  fimgmcyclem  43790  fsuppind  43811  fourierdlem42  47364  2rexsb  48377  2rexrsb  48378  pgrpgt2nabl  49683  islindeps2  49800  isldepslvec2  49802