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

Theorem ralcom 2860
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 2571 . 2  |-  F/_ y A
2 nfcv 2571 . 2  |-  F/_ x B
31, 2ralcomf 2858 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 2697
This theorem is referenced by:  ralcom4  2966  ssint  4058  iinrab2  4146  disjxun  4202  reusv3  4723  cnvpo  5402  cnvso  5403  fununi  5509  isocnv2  6043  dfsmo2  6601  ixpiin  7080  boxriin  7096  rexfiuz  12143  gcdcllem1  13003  mreacs  13875  comfeq  13924  catpropd  13927  isnsg2  14962  cntzrec  15124  oppgsubm  15150  opprirred  15799  opprsubrg  15881  tgss2  17044  ist1-2  17403  kgencn  17580  ptcnplem  17645  cnmptcom  17702  fbun  17864  cnflf  18026  fclsopn  18038  cnfcf  18066  caucfil  19228  ovolgelb  19368  dyadmax  19482  ftc1a  19913  ulmcau  20303  phoeqi  22351  ho02i  23324  hoeq2  23326  adjsym  23328  cnvadj  23387  mddmd2  23804  cdj3lem3b  23935  cvmlift2lem12  24993  dedekind  25179  dfpo2  25370  elpotr  25400  colinearalg  25841  islindf4  27276  2reu4a  27934  frgrawopreg2  28377  hbra2VD  28909  ispsubsp2  30480
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702
  Copyright terms: Public domain W3C validator