Theorem rexcom 3287

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wral 3058  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-11 2154

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-ral 3059  df-rex 3068

This theorem is referenced by:  rexcom13  3293  2reurex  3768  2reu1  3905  2reu4lem  4527  iuncom  5003  xpiundi  5758  brdom7disj  10568  addcompr  11058  mulcompr  11060  qmulz  12990  elpq  13014  caubnd2  15392  ello1mpt2  15554  o1lo1  15569  lo1add  15659  lo1mul  15660  rlimno1  15686  sqrt2irr  16281  bezoutlem2  16573  bezoutlem4  16575  pythagtriplem19  16866  lsmcom2  19687  efgrelexlemb  19782  lsmcomx  19888  pgpfac1lem2  20109  pgpfac1lem4  20112  regsep2  23399  ordthaus  23407  tgcmp  23424  txcmplem1  23664  xkococnlem  23682  regr1lem2  23763  dyadmax  25646  coeeu  26278  ostth  27697  mulscom  28179  znegscl  28392  axpasch  28970  axeuclidlem  28991  usgr2pth0  29797  elwwlks2  29995  elwspths2spth  29996  shscom  31347  mdsymlem4  32434  mdsymlem8  32438  ordtconnlem1  33884  cvmliftlem15  35282  fvineqsneq  37394  lshpsmreu  39090  islpln5  39517  islvol5  39561  paddcom  39795  mapdrvallem2  41627  hdmapglem7a  41909  remexz  42085  hashnexinjle  42110  fimgmcyclem  42519  fsuppind  42576  fourierdlem42  46104  2rexsb  47050  2rexrsb  47051  pgrpgt2nabl  48210  islindeps2  48328  isldepslvec2  48330