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

Theorem rexcom 2880
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 2577 . 2  |-  F/_ y A
2 nfcv 2577 . 2  |-  F/_ x B
31, 2rexcomf 2878 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 2714
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-cleq 2434  df-clel 2437  df-nfc 2566  df-rex 2719
This theorem is referenced by:  rexcom13  2881  rexcom4  2990  iuncom  4175  xpiundi  4891  brdom7disj  8696  addcompr  9188  mulcompr  9190  qmulz  10954  caubnd2  12843  ello1mpt2  12998  o1lo1  13013  lo1add  13102  lo1mul  13103  rlimno1  13129  sqr2irr  13529  bezoutlem2  13721  bezoutlem4  13723  pythagtriplem19  13898  lsmcom2  16152  efgrelexlemb  16245  lsmcomx  16336  pgpfac1lem2  16574  pgpfac1lem4  16577  regsep2  18978  ordthaus  18986  tgcmp  19002  txcmplem1  19212  xkococnlem  19230  regr1lem2  19311  dyadmax  21076  coeeu  21691  ostth  22886  axpasch  23185  axeuclidlem  23206  shscom  24720  mdsymlem4  25808  mdsymlem8  25812  ordtconlem1  26352  cvmliftlem15  27185  nofulllem5  27845  2rexsb  29991  2rexrsb  29992  2reurex  30002  2reu1  30007  2reu4a  30010  usgra2pth0  30299  el2wlksot  30396  el2pthsot  30397  frgrawopreglem5  30638  pgrpgt2nabel  30766  islindeps2  31014  isldepslvec2  31016  lshpsmreu  32751  islpln5  33176  islvol5  33220  paddcom  33454  mapdrvallem2  35287  hdmapglem7a  35572
  Copyright terms: Public domain W3C validator