Theorem rexcom 3267

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wral 3045  ∃wrex 3054

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 2158

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

This theorem is referenced by:  rexcom13  3273  2reurex  3734  2reu1  3863  2reu4lem  4488  iuncom  4966  xpiundi  5712  brdom7disj  10491  addcompr  10981  mulcompr  10983  qmulz  12917  elpq  12941  caubnd2  15331  ello1mpt2  15495  o1lo1  15510  lo1add  15600  lo1mul  15601  rlimno1  15627  sqrt2irr  16224  bezoutlem2  16517  bezoutlem4  16519  pythagtriplem19  16811  lsmcom2  19592  efgrelexlemb  19687  lsmcomx  19793  pgpfac1lem2  20014  pgpfac1lem4  20017  regsep2  23270  ordthaus  23278  tgcmp  23295  txcmplem1  23535  xkococnlem  23553  regr1lem2  23634  dyadmax  25506  coeeu  26137  ostth  27557  mulscom  28049  znegscl  28287  zs12negscl  28347  zs12ge0  28349  axpasch  28875  axeuclidlem  28896  usgr2pth0  29702  elwwlks2  29903  elwspths2spth  29904  shscom  31255  mdsymlem4  32342  mdsymlem8  32346  ordtconnlem1  33921  onvf1odlem1  35097  cvmliftlem15  35292  fvineqsneq  37407  lshpsmreu  39109  islpln5  39536  islvol5  39580  paddcom  39814  mapdrvallem2  41646  hdmapglem7a  41928  remexz  42099  hashnexinjle  42124  fimgmcyclem  42528  fsuppind  42585  fourierdlem42  46154  2rexsb  47106  2rexrsb  47107  pgrpgt2nabl  48358  islindeps2  48476  isldepslvec2  48478