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

Theorem ralcom 2702
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 2421 . 2  |-  F/_ y A
2 nfcv 2421 . 2  |-  F/_ x B
31, 2ralcomf 2700 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 2545
This theorem is referenced by:  ralcom4  2808  ssint  3880  iinrab2  3967  disjxun  4023  reusv3  4544  cnvpo  5215  cnvso  5216  fununi  5318  isocnv2  5830  dfsmo2  6366  ixpiin  6844  boxriin  6860  rexfiuz  11833  gcdcllem1  12692  mreacs  13562  comfeq  13611  catpropd  13614  isnsg2  14649  cntzrec  14811  oppgsubm  14837  opprirred  15486  opprsubrg  15568  tgss2  16727  ist1-2  17077  kgencn  17253  ptcnplem  17317  cnmptcom  17374  fbun  17537  cnflf  17699  fclsopn  17711  cnfcf  17739  caucfil  18711  ovolgelb  18841  dyadmax  18955  ftc1a  19386  ulmcau  19774  phoeqi  21438  ho02i  22411  hoeq2  22413  adjsym  22415  cnvadj  22474  mddmd2  22891  cdj3lem3b  23022  cvmlift2lem12  23847  dedekind  24084  dfpo2  24114  elpotr  24139  colinearalg  24540  islindf4  27319  2reu4a  27978  hbra2VD  28709  ispsubsp2  30008
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ral 2550
  Copyright terms: Public domain W3C validator