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

Theorem rexcom 2714
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 2432 . 2  |-  F/_ y A
2 nfcv 2432 . 2  |-  F/_ x B
31, 2rexcomf 2712 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 2557
This theorem is referenced by:  rexcom13  2715  rexcom4  2820  iuncom  3927  xpiundi  4759  brdom7disj  8172  addcompr  8661  mulcompr  8663  qmulz  10335  caubnd2  11857  ello1mpt2  12012  o1lo1  12027  lo1add  12116  lo1mul  12117  rlimno1  12143  sqr2irr  12543  bezoutlem2  12734  bezoutlem4  12736  pythagtriplem19  12902  lsmcom2  14982  efgrelexlemb  15075  lsmcomx  15164  pgpfac1lem2  15326  pgpfac1lem4  15329  regsep2  17120  ordthaus  17128  tgcmp  17144  txcmplem1  17351  xkococnlem  17369  regr1lem2  17447  dyadmax  18969  coeeu  19623  ostth  20804  shscom  21914  mdsymlem4  23002  mdsymlem8  23006  cvmliftlem15  23844  nofulllem5  24431  elfuns  24525  axpasch  24641  axeuclidlem  24662  iscst4  25280  2rexsb  28051  2rexrsb  28052  2reurex  28062  2reu1  28067  2reu4a  28070  lshpsmreu  29921  islpln5  30346  islvol5  30390  paddcom  30624  mapdrvallem2  32457  hdmapglem7a  32742
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rex 2562
  Copyright terms: Public domain W3C validator