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

Theorem ralcom 2700
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 2419 . 2  |-  F/_ y A
2 nfcv 2419 . 2  |-  F/_ x B
31, 2ralcomf 2698 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 2543
This theorem is referenced by:  ralcom4  2806  ssint  3878  iinrab2  3965  disjxun  4021  reusv3  4542  cnvpo  5213  cnvso  5214  fununi  5316  isocnv2  5828  dfsmo2  6364  ixpiin  6842  boxriin  6858  rexfiuz  11831  gcdcllem1  12690  mreacs  13560  comfeq  13609  catpropd  13612  isnsg2  14647  cntzrec  14809  oppgsubm  14835  opprirred  15484  opprsubrg  15566  tgss2  16725  ist1-2  17075  kgencn  17251  ptcnplem  17315  cnmptcom  17372  fbun  17535  cnflf  17697  fclsopn  17709  cnfcf  17737  caucfil  18709  ovolgelb  18839  dyadmax  18953  ftc1a  19384  ulmcau  19772  phoeqi  21436  ho02i  22409  hoeq2  22411  adjsym  22413  cnvadj  22472  mddmd2  22889  cdj3lem3b  23020  cvmlift2lem12  23845  dedekind  24082  dfpo2  24112  elpotr  24137  colinearalg  24538  islindf4  27308  2reu4a  27967  hbra2VD  28636  ispsubsp2  29935
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548
  Copyright terms: Public domain W3C validator