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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wral 3061  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-11 2157

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3062  df-rex 3071

This theorem is referenced by:  rexcom13  3296  2reurex  3766  2reu1  3897  2reu4lem  4522  iuncom  4999  xpiundi  5756  brdom7disj  10571  addcompr  11061  mulcompr  11063  qmulz  12993  elpq  13017  caubnd2  15396  ello1mpt2  15558  o1lo1  15573  lo1add  15663  lo1mul  15664  rlimno1  15690  sqrt2irr  16285  bezoutlem2  16577  bezoutlem4  16579  pythagtriplem19  16871  lsmcom2  19673  efgrelexlemb  19768  lsmcomx  19874  pgpfac1lem2  20095  pgpfac1lem4  20098  regsep2  23384  ordthaus  23392  tgcmp  23409  txcmplem1  23649  xkococnlem  23667  regr1lem2  23748  dyadmax  25633  coeeu  26264  ostth  27683  mulscom  28165  znegscl  28378  axpasch  28956  axeuclidlem  28977  usgr2pth0  29785  elwwlks2  29986  elwspths2spth  29987  shscom  31338  mdsymlem4  32425  mdsymlem8  32429  ordtconnlem1  33923  cvmliftlem15  35303  fvineqsneq  37413  lshpsmreu  39110  islpln5  39537  islvol5  39581  paddcom  39815  mapdrvallem2  41647  hdmapglem7a  41929  remexz  42105  hashnexinjle  42130  fimgmcyclem  42543  fsuppind  42600  fourierdlem42  46164  2rexsb  47113  2rexrsb  47114  pgrpgt2nabl  48282  islindeps2  48400  isldepslvec2  48402