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

Theorem ralcom 2662
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 2385 . 2  |-  F/_ y A
2 nfcv 2385 . 2  |-  F/_ x B
31, 2ralcomf 2660 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 2509
This theorem is referenced by:  ralcom4  2744  ssint  3776  iinrab2  3863  disjxun  3918  reusv3  4433  cnvpo  5119  cnvso  5120  fununi  5173  isocnv2  5680  dfsmo2  6250  ixpiin  6728  boxriin  6744  rexfiuz  11708  gcdcllem1  12564  mreacs  13404  comfeq  13453  catpropd  13456  isnsg2  14482  cntzrec  14644  oppgsubm  14670  opprirred  15319  opprsubrg  15401  tgss2  16557  ist1-2  16907  kgencn  17083  ptcnplem  17147  cnmptcom  17204  fbun  17367  cnflf  17529  fclsopn  17541  cnfcf  17569  caucfil  18541  ovolgelb  18671  dyadmax  18785  ftc1a  19216  ulmcau  19604  phoeqi  21266  ho02i  22239  hoeq2  22241  adjsym  22243  cnvadj  22302  mddmd2  22719  cdj3lem3b  22850  cvmlift2lem12  23016  dedekind  23252  dfpo2  23282  elpotr  23305  colinearalg  23712  islindf4  26474  hbra2VD  27326  ispsubsp2  28624
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 1926  ax-ext 2234
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 1883  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ral 2513
  Copyright terms: Public domain W3C validator