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

Theorem rexcom 3005
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 2605 . 2  |-  F/_ y A
2 nfcv 2605 . 2  |-  F/_ x B
31, 2rexcomf 3003 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 2794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1600  df-nf 1604  df-sb 1727  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798  df-rex 2799
This theorem is referenced by:  rexcom13  3006  rexcom4  3115  iuncom  4322  xpiundi  5044  brdom7disj  8912  addcompr  9402  mulcompr  9404  qmulz  11196  caubnd2  13172  ello1mpt2  13327  o1lo1  13342  lo1add  13431  lo1mul  13432  rlimno1  13458  sqrt2irr  13964  bezoutlem2  14159  bezoutlem4  14161  pythagtriplem19  14339  lsmcom2  16654  efgrelexlemb  16747  lsmcomx  16841  pgpfac1lem2  17105  pgpfac1lem4  17108  regsep2  19855  ordthaus  19863  tgcmp  19879  txcmplem1  20120  xkococnlem  20138  regr1lem2  20219  dyadmax  21985  coeeu  22600  ostth  23802  axpasch  24222  axeuclidlem  24243  el2wlksot  24858  el2pthsot  24859  frgrawopreglem5  25026  shscom  26215  mdsymlem4  27303  mdsymlem8  27307  ordtconlem1  27884  cvmliftlem15  28721  nofulllem5  29442  fourierdlem42  31885  2rexsb  32129  2rexrsb  32130  2reurex  32140  2reu1  32145  2reu4a  32148  usgra2pth0  32309  pgrpgt2nabl  32827  islindeps2  32954  isldepslvec2  32956  lshpsmreu  34709  islpln5  35134  islvol5  35178  paddcom  35412  mapdrvallem2  37247  hdmapglem7a  37532
  Copyright terms: Public domain W3C validator