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

Theorem ralcom 2671
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 2392 . 2  |-  F/_ y A
2 nfcv 2392 . 2  |-  F/_ x B
31, 2ralcomf 2669 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 2516
This theorem is referenced by:  ralcom4  2757  ssint  3819  iinrab2  3906  disjxun  3961  reusv3  4479  cnvpo  5165  cnvso  5166  fununi  5219  isocnv2  5727  dfsmo2  6297  ixpiin  6775  boxriin  6791  rexfiuz  11761  gcdcllem1  12617  mreacs  13487  comfeq  13536  catpropd  13539  isnsg2  14574  cntzrec  14736  oppgsubm  14762  opprirred  15411  opprsubrg  15493  tgss2  16652  ist1-2  17002  kgencn  17178  ptcnplem  17242  cnmptcom  17299  fbun  17462  cnflf  17624  fclsopn  17636  cnfcf  17664  caucfil  18636  ovolgelb  18766  dyadmax  18880  ftc1a  19311  ulmcau  19699  phoeqi  21361  ho02i  22334  hoeq2  22336  adjsym  22338  cnvadj  22397  mddmd2  22814  cdj3lem3b  22945  cvmlift2lem12  23182  dedekind  23418  dfpo2  23448  elpotr  23471  colinearalg  23878  islindf4  26640  hbra2VD  27649  ispsubsp2  29065
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 2237
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 2249  df-clel 2252  df-nfc 2381  df-ral 2520
  Copyright terms: Public domain W3C validator