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

Theorem rgen2a 2891
Description: Generalization rule for restricted quantification. Note that  x and  y needn't be distinct (and illustrates the use of dvelim 2052). (Contributed by NM, 23-Nov-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 1-Jan-2020.) (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 2539 . . . . . 6  |-  ( z  =  x  ->  (
z  e.  A  <->  x  e.  A ) )
21dvelimv 2053 . . . . 5  |-  ( -. 
A. y  y  =  x  ->  ( x  e.  A  ->  A. y  x  e.  A )
)
3 rgen2a.1 . . . . . . 7  |-  ( ( x  e.  A  /\  y  e.  A )  ->  ph )
43ex 434 . . . . . 6  |-  ( x  e.  A  ->  (
y  e.  A  ->  ph ) )
54alimi 1614 . . . . 5  |-  ( A. y  x  e.  A  ->  A. y ( y  e.  A  ->  ph )
)
62, 5syl6com 35 . . . 4  |-  ( x  e.  A  ->  ( -.  A. y  y  =  x  ->  A. y
( y  e.  A  ->  ph ) ) )
7 eleq1 2539 . . . . . . 7  |-  ( y  =  x  ->  (
y  e.  A  <->  x  e.  A ) )
87biimpd 207 . . . . . 6  |-  ( y  =  x  ->  (
y  e.  A  ->  x  e.  A )
)
98, 4syli 37 . . . . 5  |-  ( y  =  x  ->  (
y  e.  A  ->  ph ) )
109alimi 1614 . . . 4  |-  ( A. y  y  =  x  ->  A. y ( y  e.  A  ->  ph )
)
116, 10pm2.61d2 160 . . 3  |-  ( x  e.  A  ->  A. y
( y  e.  A  ->  ph ) )
12 df-ral 2819 . . 3  |-  ( A. y  e.  A  ph  <->  A. y
( y  e.  A  ->  ph ) )
1311, 12sylibr 212 . 2  |-  ( x  e.  A  ->  A. y  e.  A  ph )
1413rgen 2824 1  |-  A. x  e.  A  A. y  e.  A  ph
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369   A.wal 1377    e. wcel 1767   A.wral 2814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-nf 1600  df-cleq 2459  df-clel 2462  df-ral 2819
This theorem is referenced by:  sosn  5069  isoid  6214  f1owe  6238  ordon  6603  fnwelem  6899  issmo  7020  oawordeulem  7204  ecopover  7416  unfilem2  7786  dffi2  7884  inficl  7886  fipwuni  7887  fisn  7888  dffi3  7892  cantnfvalf  8085  r111  8194  alephf1  8467  alephiso  8480  dfac5lem4  8508  kmlem9  8539  ackbij1lem17  8617  fin1a2lem2  8782  fin1a2lem4  8784  axcc2lem  8817  nqereu  9308  addpqf  9323  mulpqf  9325  genpdm  9381  axaddf  9523  axmulf  9524  subf  9823  mulnzcnopr  10196  negiso  10520  cnref1o  11216  xaddf  11424  xmulf  11465  ioof  11623  om2uzf1oi  12033  om2uzisoi  12034  wwlktovf1  12861  reeff1  13719  divalglem9  13921  bitsf1  13958  gcdf  14019  eucalgf  14074  qredeu  14110  1arith  14307  vdwapf  14352  catideu  14933  sscres  15056  fpwipodrs  15654  letsr  15717  mgmidmo  15738  frmdplusg  15857  nmznsg  16059  efgred  16581  isabli  16627  brric  17205  xrs1cmn  18266  xrge0subm  18267  xrsds  18269  cnsubmlem  18274  cnsubrglem  18276  fibas  19285  fctop  19311  cctop  19313  iccordt  19521  fsubbas  20195  zfbas  20224  ismeti  20655  dscmet  20920  qtopbaslem  21092  tgqioo  21132  xrsxmet  21141  xrsdsre  21142  retopcon  21161  iccconn  21162  iimulcn  21265  icopnfhmeo  21270  iccpnfhmeo  21272  xrhmeo  21273  iundisj2  21786  reefiso  22669  recosf1o  22747  rzgrp  22766  isabloi  25063  issubgoi  25085  exidu1  25101  rngoideu  25159  cncph  25507  hvsubf  25705  hhip  25867  hhph  25868  helch  25934  hsn0elch  25939  hhshsslem2  25957  shscli  26008  shintcli  26020  pjmf1  26407  idunop  26670  idhmop  26674  0hmop  26675  adj0  26686  lnopunii  26704  lnophmi  26710  riesz4i  26755  cnlnadjlem9  26767  adjcoi  26792  bra11  26800  pjhmopi  26838  iundisj2f  27219  iundisj2fi  27367  xrstos  27426  xrge0omnd  27460  reofld  27590  xrge0slmod  27594  iistmd  27635  cnre2csqima  27644  mndpluscn  27659  raddcn  27662  xrge0iifiso  27668  xrge0iifmhm  27672  xrge0pluscn  27673  br2base  27991  sxbrsiga  28012  indispcon  28430  iooscon  28443  ghomsn  28779  soseq  29187  mzpclall  30490  kelac2lem  30841  isomliN  34253  idlaut  35109
  Copyright terms: Public domain W3C validator