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

Theorem rexcom 2701
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 2419 . 2  |-  F/_ y A
2 nfcv 2419 . 2  |-  F/_ x B
31, 2rexcomf 2699 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 176   E.wrex 2544
This theorem is referenced by:  rexcom13  2702  rexcom4  2807  iuncom  3911  xpiundi  4743  brdom7disj  8156  addcompr  8645  mulcompr  8647  qmulz  10319  caubnd2  11841  ello1mpt2  11996  o1lo1  12011  lo1add  12100  lo1mul  12101  rlimno1  12127  sqr2irr  12527  bezoutlem2  12718  bezoutlem4  12720  pythagtriplem19  12886  lsmcom2  14966  efgrelexlemb  15059  lsmcomx  15148  pgpfac1lem2  15310  pgpfac1lem4  15313  regsep2  17104  ordthaus  17112  tgcmp  17128  txcmplem1  17335  xkococnlem  17353  regr1lem2  17431  dyadmax  18953  coeeu  19607  ostth  20788  shscom  21898  mdsymlem4  22986  mdsymlem8  22990  cvmliftlem15  23829  nofulllem5  24360  elfuns  24454  axpasch  24569  axeuclidlem  24590  iscst4  25177  2rexsb  27948  2rexrsb  27949  2reurex  27959  2reu1  27964  2reu4a  27967  lshpsmreu  29299  islpln5  29724  islvol5  29768  paddcom  30002  mapdrvallem2  31835  hdmapglem7a  32120
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549
  Copyright terms: Public domain W3C validator