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

Theorem ralcom 2713
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 2432 . 2  |-  F/_ y A
2 nfcv 2432 . 2  |-  F/_ x B
31, 2ralcomf 2711 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 2556
This theorem is referenced by:  ralcom4  2819  ssint  3894  iinrab2  3981  disjxun  4037  reusv3  4558  cnvpo  5229  cnvso  5230  fununi  5332  isocnv2  5844  dfsmo2  6380  ixpiin  6858  boxriin  6874  rexfiuz  11847  gcdcllem1  12706  mreacs  13576  comfeq  13625  catpropd  13628  isnsg2  14663  cntzrec  14825  oppgsubm  14851  opprirred  15500  opprsubrg  15582  tgss2  16741  ist1-2  17091  kgencn  17267  ptcnplem  17331  cnmptcom  17388  fbun  17551  cnflf  17713  fclsopn  17725  cnfcf  17753  caucfil  18725  ovolgelb  18855  dyadmax  18969  ftc1a  19400  ulmcau  19788  phoeqi  21452  ho02i  22425  hoeq2  22427  adjsym  22429  cnvadj  22488  mddmd2  22905  cdj3lem3b  23036  cvmlift2lem12  23860  dedekind  24097  dfpo2  24183  elpotr  24208  colinearalg  24610  islindf4  27411  2reu4a  28070  hbra2VD  28952  ispsubsp2  30557
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561
  Copyright terms: Public domain W3C validator