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

Theorem ralcom 2701
Description: Commutation of restricted quantifiers. (Contributed by NM, 13-Oct-1999.) (Revised by Mario Carneiro, 14-Oct-2016.)
Assertion
Ref Expression
ralcom  |-  ( A. x  e.  A  A. y  e.  B  ph  <->  A. y  e.  B  A. 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 ralcom
StepHypRef Expression
1 nfcv 2420 . 2  |-  F/_ y A
2 nfcv 2420 . 2  |-  F/_ x B
31, 2ralcomf 2699 1  |-  ( A. x  e.  A  A. y  e.  B  ph  <->  A. y  e.  B  A. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 176   A.wral 2544
This theorem is referenced by:  ralcom4  2807  ssint  3879  iinrab2  3966  disjxun  4022  reusv3  4541  cnvpo  5211  cnvso  5212  fununi  5282  isocnv2  5790  dfsmo2  6360  ixpiin  6838  boxriin  6854  rexfiuz  11827  gcdcllem1  12686  mreacs  13556  comfeq  13605  catpropd  13608  isnsg2  14643  cntzrec  14805  oppgsubm  14831  opprirred  15480  opprsubrg  15562  tgss2  16721  ist1-2  17071  kgencn  17247  ptcnplem  17311  cnmptcom  17368  fbun  17531  cnflf  17693  fclsopn  17705  cnfcf  17733  caucfil  18705  ovolgelb  18835  dyadmax  18949  ftc1a  19380  ulmcau  19768  phoeqi  21430  ho02i  22405  hoeq2  22407  adjsym  22409  cnvadj  22468  mddmd2  22885  cdj3lem3b  23016  cvmlift2lem12  23252  dedekind  23488  dfpo2  23518  elpotr  23541  colinearalg  23948  islindf4  26719  2reu4a  27358  hbra2VD  27916  ispsubsp2  29214
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 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
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 1631  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ral 2549
  Copyright terms: Public domain W3C validator