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

Theorem ralcom 2811
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 2523 . 2  |-  F/_ y A
2 nfcv 2523 . 2  |-  F/_ x B
31, 2ralcomf 2809 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 177   A.wral 2649
This theorem is referenced by:  ralcom4  2917  ssint  4008  iinrab2  4095  disjxun  4151  reusv3  4671  cnvpo  5350  cnvso  5351  fununi  5457  isocnv2  5990  dfsmo2  6545  ixpiin  7024  boxriin  7040  rexfiuz  12078  gcdcllem1  12938  mreacs  13810  comfeq  13859  catpropd  13862  isnsg2  14897  cntzrec  15059  oppgsubm  15085  opprirred  15734  opprsubrg  15816  tgss2  16975  ist1-2  17333  kgencn  17509  ptcnplem  17574  cnmptcom  17631  fbun  17793  cnflf  17955  fclsopn  17967  cnfcf  17995  caucfil  19107  ovolgelb  19243  dyadmax  19357  ftc1a  19788  ulmcau  20178  phoeqi  22207  ho02i  23180  hoeq2  23182  adjsym  23184  cnvadj  23243  mddmd2  23660  cdj3lem3b  23791  cvmlift2lem12  24780  dedekind  24966  dfpo2  25136  elpotr  25161  colinearalg  25563  islindf4  26977  2reu4a  27635  frgrawopreg2  27803  hbra2VD  28313  ispsubsp2  29860
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ral 2654
  Copyright terms: Public domain W3C validator