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

Theorem rexcom 2869
Description: Commutation of restricted 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 2572 . 2  |-  F/_ y A
2 nfcv 2572 . 2  |-  F/_ x B
31, 2rexcomf 2867 1  |-  ( E. x  e.  A  E. y  e.  B  ph  <->  E. y  e.  B  E. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 177   E.wrex 2706
This theorem is referenced by:  rexcom13  2870  rexcom4  2975  iuncom  4099  xpiundi  4932  brdom7disj  8409  addcompr  8898  mulcompr  8900  qmulz  10577  caubnd2  12161  ello1mpt2  12316  o1lo1  12331  lo1add  12420  lo1mul  12421  rlimno1  12447  sqr2irr  12848  bezoutlem2  13039  bezoutlem4  13041  pythagtriplem19  13207  lsmcom2  15289  efgrelexlemb  15382  lsmcomx  15471  pgpfac1lem2  15633  pgpfac1lem4  15636  regsep2  17440  ordthaus  17448  tgcmp  17464  txcmplem1  17673  xkococnlem  17691  regr1lem2  17772  dyadmax  19490  coeeu  20144  ostth  21333  shscom  22821  mdsymlem4  23909  mdsymlem8  23913  cvmliftlem15  24985  nofulllem5  25661  axpasch  25880  axeuclidlem  25901  2rexsb  27924  2rexrsb  27925  2reurex  27935  2reu1  27940  2reu4a  27943  usgra2pth0  28312  el2wlksot  28347  el2pthsot  28348  frgrawopreglem5  28437  lshpsmreu  29907  islpln5  30332  islvol5  30376  paddcom  30610  mapdrvallem2  32443  hdmapglem7a  32728
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rex 2711
  Copyright terms: Public domain W3C validator