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

Theorem ralcom 2673
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 2671 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  2774  ssint  3838  iinrab2  3925  disjxun  3981  reusv3  4500  cnvpo  5186  cnvso  5187  fununi  5240  isocnv2  5748  dfsmo2  6318  ixpiin  6796  boxriin  6812  rexfiuz  11782  gcdcllem1  12638  mreacs  13508  comfeq  13557  catpropd  13560  isnsg2  14595  cntzrec  14757  oppgsubm  14783  opprirred  15432  opprsubrg  15514  tgss2  16673  ist1-2  17023  kgencn  17199  ptcnplem  17263  cnmptcom  17320  fbun  17483  cnflf  17645  fclsopn  17657  cnfcf  17685  caucfil  18657  ovolgelb  18787  dyadmax  18901  ftc1a  19332  ulmcau  19720  phoeqi  21382  ho02i  22355  hoeq2  22357  adjsym  22359  cnvadj  22418  mddmd2  22835  cdj3lem3b  22966  cvmlift2lem12  23203  dedekind  23439  dfpo2  23469  elpotr  23492  colinearalg  23899  islindf4  26661  hbra2VD  27670  ispsubsp2  29086
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 2521
  Copyright terms: Public domain W3C validator