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

Theorem ralcom 2813
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 2525 . 2  |-  F/_ y A
2 nfcv 2525 . 2  |-  F/_ x B
31, 2ralcomf 2811 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 2651
This theorem is referenced by:  ralcom4  2919  ssint  4010  iinrab2  4097  disjxun  4153  reusv3  4673  cnvpo  5352  cnvso  5353  fununi  5459  isocnv2  5992  dfsmo2  6547  ixpiin  7026  boxriin  7042  rexfiuz  12080  gcdcllem1  12940  mreacs  13812  comfeq  13861  catpropd  13864  isnsg2  14899  cntzrec  15061  oppgsubm  15087  opprirred  15736  opprsubrg  15818  tgss2  16977  ist1-2  17335  kgencn  17511  ptcnplem  17576  cnmptcom  17633  fbun  17795  cnflf  17957  fclsopn  17969  cnfcf  17997  caucfil  19109  ovolgelb  19245  dyadmax  19359  ftc1a  19790  ulmcau  20180  phoeqi  22209  ho02i  23182  hoeq2  23184  adjsym  23186  cnvadj  23245  mddmd2  23662  cdj3lem3b  23793  cvmlift2lem12  24782  dedekind  24968  dfpo2  25138  elpotr  25163  colinearalg  25565  islindf4  26979  2reu4a  27637  frgrawopreg2  27805  hbra2VD  28315  ispsubsp2  29862
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 2370
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 2382  df-clel 2385  df-nfc 2514  df-ral 2656
  Copyright terms: Public domain W3C validator