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

Theorem rgen2a 2715
Description: Generalization rule for restricted quantification. Note that  x and  y needn't be distinct (and illustrates the use of dvelim 2050). (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 2447 . . . . . . . 8  |-  ( y  =  x  ->  (
y  e.  A  <->  x  e.  A ) )
2 rgen2a.1 . . . . . . . . 9  |-  ( ( x  e.  A  /\  y  e.  A )  ->  ph )
32ex 424 . . . . . . . 8  |-  ( x  e.  A  ->  (
y  e.  A  ->  ph ) )
41, 3syl6bi 220 . . . . . . 7  |-  ( y  =  x  ->  (
y  e.  A  -> 
( y  e.  A  ->  ph ) ) )
54pm2.43d 46 . . . . . 6  |-  ( y  =  x  ->  (
y  e.  A  ->  ph ) )
65alimi 1565 . . . . 5  |-  ( A. y  y  =  x  ->  A. y ( y  e.  A  ->  ph )
)
76a1d 23 . . . 4  |-  ( A. y  y  =  x  ->  ( x  e.  A  ->  A. y ( y  e.  A  ->  ph )
) )
8 eleq1 2447 . . . . . 6  |-  ( z  =  x  ->  (
z  e.  A  <->  x  e.  A ) )
98dvelimv 1975 . . . . 5  |-  ( -. 
A. y  y  =  x  ->  ( x  e.  A  ->  A. y  x  e.  A )
)
103alimi 1565 . . . . 5  |-  ( A. y  x  e.  A  ->  A. y ( y  e.  A  ->  ph )
)
119, 10syl6 31 . . . 4  |-  ( -. 
A. y  y  =  x  ->  ( x  e.  A  ->  A. y
( y  e.  A  ->  ph ) ) )
127, 11pm2.61i 158 . . 3  |-  ( x  e.  A  ->  A. y
( y  e.  A  ->  ph ) )
13 df-ral 2654 . . 3  |-  ( A. y  e.  A  ph  <->  A. y
( y  e.  A  ->  ph ) )
1412, 13sylibr 204 . 2  |-  ( x  e.  A  ->  A. y  e.  A  ph )
1514rgen 2714 1  |-  A. x  e.  A  A. y  e.  A  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 359   A.wal 1546    e. wcel 1717   A.wral 2649
This theorem is referenced by:  ordon  4703  sosn  4887  isoid  5988  f1owe  6012  fnwelem  6397  issmo  6546  oawordeulem  6733  ecopover  6944  unfilem2  7308  dffi2  7363  inficl  7365  fipwuni  7366  fisn  7367  dffi3  7371  cantnfvalf  7553  r111  7634  alephf1  7899  alephiso  7912  dfac5lem4  7940  kmlem9  7971  ackbij1lem17  8049  fin1a2lem2  8214  fin1a2lem4  8216  axcc2lem  8249  nqereu  8739  addpqf  8754  mulpqf  8756  genpdm  8812  axaddf  8953  axmulf  8954  subf  9239  mulnzcnopr  9600  negiso  9916  cnref1o  10539  xaddf  10742  xmulf  10783  ioof  10934  om2uzf1oi  11220  om2uzisoi  11221  reeff1  12648  divalglem9  12848  bitsf1  12885  gcdf  12946  eucalgf  13001  qredeu  13034  1arith  13222  vdwapf  13267  catideu  13827  sscres  13950  islati  14408  fpwipodrs  14517  letsr  14599  mgmidmo  14620  frmdplusg  14726  nmznsg  14911  efgred  15307  isabli  15353  xrs1cmn  16661  xrge0subm  16662  xrsds  16664  cnsubmlem  16669  cnsubrglem  16671  fibas  16965  fctop  16991  cctop  16993  iccordt  17200  fsubbas  17820  zfbas  17849  ismeti  18264  dscmet  18491  qtopbaslem  18663  tgqioo  18702  xrsxmet  18711  xrsdsre  18712  retopcon  18731  iccconn  18732  iimulcn  18834  icopnfhmeo  18839  iccpnfhmeo  18841  xrhmeo  18842  iundisj2  19310  reefiso  20231  recosf1o  20304  isabloi  21724  issubgoi  21746  exidu1  21762  rngoideu  21820  cncph  22168  hvsubf  22366  hhip  22527  hhph  22528  helch  22594  hsn0elch  22598  hhshsslem2  22616  shscli  22667  shintcli  22679  pjmf1  23066  idunop  23329  idhmop  23333  0hmop  23334  adj0  23345  lnopunii  23363  lnophmi  23369  riesz4i  23414  cnlnadjlem9  23426  adjcoi  23451  bra11  23459  pjhmopi  23497  iundisj2f  23873  iundisj2fi  23991  reofld  24096  iistmd  24104  cnre2csqima  24113  mndpluscn  24116  raddcn  24119  xrge0iifiso  24125  xrge0iifmhm  24129  xrge0pluscn  24130  br2base  24413  sxbrsiga  24434  indispcon  24700  iooscon  24713  ghomsn  24878  soseq  25278  mzpclall  26475  kelac2lem  26831  isopiN  29296  isomliN  29354  idlaut  30210
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-cleq 2380  df-clel 2383  df-ral 2654
  Copyright terms: Public domain W3C validator