MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexcom Structured version   Unicode version

Theorem rexcom 2944
Description: Commutation of restricted existential quantifiers. (Contributed by NM, 19-Nov-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)
Assertion
Ref Expression
rexcom  |-  ( E. x  e.  A  E. y  e.  B  ph  <->  E. y  e.  B  E. x  e.  A  ph )
Distinct variable groups:    x, y    x, B    y, A
Allowed substitution hints:    ph( x, y)    A( x)    B( y)

Proof of Theorem rexcom
StepHypRef Expression
1 nfcv 2544 . 2  |-  F/_ y A
2 nfcv 2544 . 2  |-  F/_ x B
31, 2rexcomf 2942 1  |-  ( E. x  e.  A  E. y  e.  B  ph  <->  E. y  e.  B  E. x  e.  A  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   E.wrex 2733
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-ex 1621  df-nf 1625  df-sb 1748  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ral 2737  df-rex 2738
This theorem is referenced by:  rexcom13  2945  rexcom4  3054  iuncom  4250  xpiundi  4968  brdom7disj  8822  addcompr  9310  mulcompr  9312  qmulz  11104  caubnd2  13192  ello1mpt2  13347  o1lo1  13362  lo1add  13451  lo1mul  13452  rlimno1  13478  sqrt2irr  13984  bezoutlem2  14179  bezoutlem4  14181  pythagtriplem19  14359  lsmcom2  16792  efgrelexlemb  16885  lsmcomx  16979  pgpfac1lem2  17239  pgpfac1lem4  17242  regsep2  19963  ordthaus  19971  tgcmp  19987  txcmplem1  20227  xkococnlem  20245  regr1lem2  20326  dyadmax  22092  coeeu  22707  ostth  23941  axpasch  24365  axeuclidlem  24386  el2wlksot  25001  el2pthsot  25002  frgrawopreglem5  25169  shscom  26354  mdsymlem4  27441  mdsymlem8  27445  ordtconlem1  28060  cvmliftlem15  28932  nofulllem5  29631  fourierdlem42  32097  2rexsb  32341  2rexrsb  32342  2reurex  32352  2reu1  32357  2reu4a  32360  usgra2pth0  32673  pgrpgt2nabl  33159  islindeps2  33284  isldepslvec2  33286  lshpsmreu  35247  islpln5  35672  islvol5  35716  paddcom  35950  mapdrvallem2  37785  hdmapglem7a  38070
  Copyright terms: Public domain W3C validator