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

Theorem rgen2a 2609
Description: Generalization rule for restricted quantification. Note that  x and  y needn't be distinct (and illustrates the use of dvelim 1956). (Contributed by NM, 23-Nov-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.
Hypothesis
Ref Expression
rgen2a.1  |-  ( ( x  e.  A  /\  y  e.  A )  ->  ph )
Assertion
Ref Expression
rgen2a  |-  A. x  e.  A  A. y  e.  A  ph
Distinct variable group:    y, A
Allowed substitution hints:    ph( x, y)    A( x)

Proof of Theorem rgen2a
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 eleq1 2343 . . . . . . . 8  |-  ( y  =  x  ->  (
y  e.  A  <->  x  e.  A ) )
2 rgen2a.1 . . . . . . . . 9  |-  ( ( x  e.  A  /\  y  e.  A )  ->  ph )
32ex 423 . . . . . . . 8  |-  ( x  e.  A  ->  (
y  e.  A  ->  ph ) )
41, 3syl6bi 219 . . . . . . 7  |-  ( y  =  x  ->  (
y  e.  A  -> 
( y  e.  A  ->  ph ) ) )
54pm2.43d 44 . . . . . 6  |-  ( y  =  x  ->  (
y  e.  A  ->  ph ) )
65alimi 1546 . . . . 5  |-  ( A. y  y  =  x  ->  A. y ( y  e.  A  ->  ph )
)
76a1d 22 . . . 4  |-  ( A. y  y  =  x  ->  ( x  e.  A  ->  A. y ( y  e.  A  ->  ph )
) )
8 eleq1 2343 . . . . . 6  |-  ( z  =  x  ->  (
z  e.  A  <->  x  e.  A ) )
98dvelimv 1879 . . . . 5  |-  ( -. 
A. y  y  =  x  ->  ( x  e.  A  ->  A. y  x  e.  A )
)
103alimi 1546 . . . . 5  |-  ( A. y  x  e.  A  ->  A. y ( y  e.  A  ->  ph )
)
119, 10syl6 29 . . . 4  |-  ( -. 
A. y  y  =  x  ->  ( x  e.  A  ->  A. y
( y  e.  A  ->  ph ) ) )
127, 11pm2.61i 156 . . 3  |-  ( x  e.  A  ->  A. y
( y  e.  A  ->  ph ) )
13 df-ral 2548 . . 3  |-  ( A. y  e.  A  ph  <->  A. y
( y  e.  A  ->  ph ) )
1412, 13sylibr 203 . 2  |-  ( x  e.  A  ->  A. y  e.  A  ph )
1514rgen 2608 1  |-  A. x  e.  A  A. y  e.  A  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358   A.wal 1527    = wceq 1623    e. wcel 1684   A.wral 2543
This theorem is referenced by:  ordon  4574  sosn  4759  isoid  5826  f1owe  5850  fnwelem  6230  issmo  6365  oawordeulem  6552  ecopover  6762  unfilem2  7122  dffi2  7176  inficl  7178  fipwuni  7179  fisn  7180  dffi3  7184  cantnfvalf  7366  r111  7447  alephf1  7712  alephiso  7725  dfac5lem4  7753  kmlem9  7784  ackbij1lem17  7862  fin1a2lem2  8027  fin1a2lem4  8029  axcc2lem  8062  nqereu  8553  addpqf  8568  mulpqf  8570  genpdm  8626  axaddf  8767  axmulf  8768  subf  9053  mulnzcnopr  9414  negiso  9730  cnref1o  10349  xaddf  10551  xmulf  10592  ioof  10741  om2uzf1oi  11016  om2uzisoi  11017  reeff1  12400  divalglem9  12600  bitsf1  12637  gcdf  12698  eucalgf  12753  qredeu  12786  1arith  12974  vdwapf  13019  catideu  13577  islati  14158  fpwipodrs  14267  letsr  14349  mgmidmo  14370  frmdplusg  14476  nmznsg  14661  efgred  15057  isabli  15103  xrs1cmn  16411  xrge0subm  16412  xrsds  16414  cnsubmlem  16419  cnsubrglem  16421  fibas  16715  fctop  16741  cctop  16743  iccordt  16944  fsubbas  17562  zfbas  17591  ismeti  17890  dscmet  18095  qtopbaslem  18267  tgqioo  18306  xrsxmet  18315  xrsdsre  18316  retopcon  18334  iccconn  18335  iimulcn  18436  icopnfhmeo  18441  iccpnfhmeo  18443  xrhmeo  18444  iundisj2  18906  reefiso  19824  recosf1o  19897  isabloi  20955  issubgoi  20977  exidu1  20993  rngoideu  21051  cncph  21397  hvsubf  21595  hhip  21756  hhph  21757  helch  21823  hsn0elch  21827  hhshsslem2  21845  shscli  21896  shintcli  21908  pjmf1  22295  idunop  22558  idhmop  22562  0hmop  22563  adj0  22574  lnopunii  22592  lnophmi  22598  riesz4i  22643  cnlnadjlem9  22655  adjcoi  22680  bra11  22688  pjhmopi  22726  iistmd  23286  cnre2csqima  23295  mndpluscn  23299  raddcn  23302  xrge0iifmhm  23321  xrge0pluscn  23322  iundisj2fi  23364  iundisj2f  23366  br2base  23574  indispcon  23765  iooscon  23778  ghomsn  23995  soseq  24254  zintdom  25438  hmeogrpi  25536  1ded  25738  mzpclall  26805  kelac2lem  27162  isopiN  29371  isomliN  29429  idlaut  30285
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-an 360  df-ex 1529  df-cleq 2276  df-clel 2279  df-ral 2548
  Copyright terms: Public domain W3C validator