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

Theorem ralcom 2675
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 2394 . 2  |-  F/_ y A
2 nfcv 2394 . 2  |-  F/_ x B
31, 2ralcomf 2673 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 178   A.wral 2518
This theorem is referenced by:  ralcom4  2781  ssint  3852  iinrab2  3939  disjxun  3995  reusv3  4514  cnvpo  5200  cnvso  5201  fununi  5254  isocnv2  5762  dfsmo2  6332  ixpiin  6810  boxriin  6826  rexfiuz  11797  gcdcllem1  12653  mreacs  13523  comfeq  13572  catpropd  13575  isnsg2  14610  cntzrec  14772  oppgsubm  14798  opprirred  15447  opprsubrg  15529  tgss2  16688  ist1-2  17038  kgencn  17214  ptcnplem  17278  cnmptcom  17335  fbun  17498  cnflf  17660  fclsopn  17672  cnfcf  17700  caucfil  18672  ovolgelb  18802  dyadmax  18916  ftc1a  19347  ulmcau  19735  phoeqi  21397  ho02i  22370  hoeq2  22372  adjsym  22374  cnvadj  22433  mddmd2  22850  cdj3lem3b  22981  cvmlift2lem12  23218  dedekind  23454  dfpo2  23484  elpotr  23507  colinearalg  23914  islindf4  26676  2reu4a  27316  hbra2VD  27769  ispsubsp2  29185
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ral 2523
  Copyright terms: Public domain W3C validator