Theorem rexcom 3099

Description: Commutation of restricted existential quantifiers. (Contributed by NM, 19-Nov-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)

Assertion

Ref	Expression
rexcom	⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)

Distinct variable groups:   𝑥,𝑦   𝑥,𝐵   𝑦,𝐴

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑦)

Proof of Theorem rexcom

Step	Hyp	Ref	Expression
1		nfcv 2764	. 2 ⊢ Ⅎ𝑦𝐴
2		nfcv 2764	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	rexcomf 3097	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   ↔ wb 196  ∃wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918

This theorem is referenced by:  rexcom13  3101  rexcom4  3225  iuncom  4527  xpiundi  5173  brdom7disj  9353  addcompr  9843  mulcompr  9845  qmulz  11791  caubnd2  14097  ello1mpt2  14253  o1lo1  14268  lo1add  14357  lo1mul  14358  rlimno1  14384  sqrt2irr  14979  bezoutlem2  15257  bezoutlem4  15259  pythagtriplem19  15538  lsmcom2  18070  efgrelexlemb  18163  lsmcomx  18259  pgpfac1lem2  18474  pgpfac1lem4  18477  regsep2  21180  ordthaus  21188  tgcmp  21204  txcmplem1  21444  xkococnlem  21462  regr1lem2  21543  dyadmax  23366  coeeu  23981  ostth  25328  axpasch  25821  axeuclidlem  25842  usgr2pth0  26661  elwwlks2  26861  elwspths2spth  26862  shscom  28178  mdsymlem4  29265  mdsymlem8  29269  ordtconnlem1  29970  cvmliftlem15  31280  lshpsmreu  34396  islpln5  34821  islvol5  34865  paddcom  35099  mapdrvallem2  36934  hdmapglem7a  37219  fourierdlem42  40366  2rexsb  41170  2rexrsb  41171  2reurex  41181  2reu1  41186  2reu4a  41189  pgrpgt2nabl  42147  islindeps2  42272  isldepslvec2  42274