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

Theorem rexcom 3016
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 2622 . 2  |-  F/_ y A
2 nfcv 2622 . 2  |-  F/_ x B
31, 2rexcomf 3014 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 2808
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1592  df-nf 1595  df-sb 1707  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ral 2812  df-rex 2813
This theorem is referenced by:  rexcom13  3017  rexcom4  3126  iuncom  4325  xpiundi  5046  brdom7disj  8898  addcompr  9388  mulcompr  9390  qmulz  11174  caubnd2  13139  ello1mpt2  13294  o1lo1  13309  lo1add  13398  lo1mul  13399  rlimno1  13425  sqr2irr  13832  bezoutlem2  14025  bezoutlem4  14027  pythagtriplem19  14205  lsmcom2  16464  efgrelexlemb  16557  lsmcomx  16648  pgpfac1lem2  16909  pgpfac1lem4  16912  regsep2  19636  ordthaus  19644  tgcmp  19660  txcmplem1  19870  xkococnlem  19888  regr1lem2  19969  dyadmax  21735  coeeu  22350  ostth  23545  axpasch  23913  axeuclidlem  23934  el2wlksot  24542  el2pthsot  24543  frgrawopreglem5  24711  shscom  25899  mdsymlem4  26987  mdsymlem8  26991  ordtconlem1  27528  cvmliftlem15  28369  nofulllem5  29029  fourierdlem42  31404  2rexsb  31597  2rexrsb  31598  2reurex  31608  2reu1  31613  2reu4a  31616  usgra2pth0  31779  pgrpgt2nabl  31899  islindeps2  32032  isldepslvec2  32034  lshpsmreu  33781  islpln5  34206  islvol5  34250  paddcom  34484  mapdrvallem2  36317  hdmapglem7a  36602
  Copyright terms: Public domain W3C validator