Theorem rexcom 3294

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

Syntax hints:  ¬ wn 3   ↔ wb 209  ∀wral 3079  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-11 2192

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-ral 3080  df-rex 3090

This theorem is referenced by:  rexcom13  3298  2reurex  3724  2reu1  3852  2reu4lem  4485  iuncom  4965  xpiundi  5734  brdom7disj  10516  addcompr  11007  mulcompr  11009  qmulz  12976  elpq  13000  caubnd2  15411  ello1mpt2  15575  o1lo1  15590  lo1add  15680  lo1mul  15681  rlimno1  15707  sqrt2irr  16306  bezoutlem2  16599  bezoutlem4  16601  pythagtriplem19  16894  lsmcom2  19726  efgrelexlemb  19821  lsmcomx  19927  pgpfac1lem2  20148  pgpfac1lem4  20151  regsep2  23514  ordthaus  23522  tgcmp  23539  txcmplem1  23779  xkococnlem  23797  regr1lem2  23878  dyadmax  25738  coeeu  26363  ostth  27781  mulscom  28310  znegscl  28563  z12negscl  28649  z12sge0  28654  axpasch  29269  axeuclidlem  29290  usgr2pth0  30092  elwwlks2  30296  elwspths2spth  30297  shscom  31649  mdsymlem4  32736  mdsymlem8  32740  ordtconnlem1  34292  onvf1odlem1  35565  cvmliftlem15  35768  fvineqsneq  38036  lshpsmreu  39861  islpln5  40287  islvol5  40331  paddcom  40565  mapdrvallem2  42397  hdmapglem7a  42679  remexz  42849  hashnexinjle  42874  fimgmcyclem  43281  fsuppind  43302  fourierdlem42  46843  2rexsb  47815  2rexrsb  47816  pgrpgt2nabl  49123  islindeps2  49240  isldepslvec2  49242