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

Theorem rgen2a 2622
Description: Generalization rule for restricted quantification. Note that  x and  y needn't be distinct (and illustrates the use of dvelim 1969). (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 2356 . . . . . . . 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 1549 . . . . 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 2356 . . . . . 6  |-  ( z  =  x  ->  (
z  e.  A  <->  x  e.  A ) )
98dvelimv 1892 . . . . 5  |-  ( -. 
A. y  y  =  x  ->  ( x  e.  A  ->  A. y  x  e.  A )
)
103alimi 1549 . . . . 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 2561 . . 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 2621 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 1530    = wceq 1632    e. wcel 1696   A.wral 2556
This theorem is referenced by:  ordon  4590  sosn  4775  isoid  5842  f1owe  5866  fnwelem  6246  issmo  6381  oawordeulem  6568  ecopover  6778  unfilem2  7138  dffi2  7192  inficl  7194  fipwuni  7195  fisn  7196  dffi3  7200  cantnfvalf  7382  r111  7463  alephf1  7728  alephiso  7741  dfac5lem4  7769  kmlem9  7800  ackbij1lem17  7878  fin1a2lem2  8043  fin1a2lem4  8045  axcc2lem  8078  nqereu  8569  addpqf  8584  mulpqf  8586  genpdm  8642  axaddf  8783  axmulf  8784  subf  9069  mulnzcnopr  9430  negiso  9746  cnref1o  10365  xaddf  10567  xmulf  10608  ioof  10757  om2uzf1oi  11032  om2uzisoi  11033  reeff1  12416  divalglem9  12616  bitsf1  12653  gcdf  12714  eucalgf  12769  qredeu  12802  1arith  12990  vdwapf  13035  catideu  13593  islati  14174  fpwipodrs  14283  letsr  14365  mgmidmo  14386  frmdplusg  14492  nmznsg  14677  efgred  15073  isabli  15119  xrs1cmn  16427  xrge0subm  16428  xrsds  16430  cnsubmlem  16435  cnsubrglem  16437  fibas  16731  fctop  16757  cctop  16759  iccordt  16960  fsubbas  17578  zfbas  17607  ismeti  17906  dscmet  18111  qtopbaslem  18283  tgqioo  18322  xrsxmet  18331  xrsdsre  18332  retopcon  18350  iccconn  18351  iimulcn  18452  icopnfhmeo  18457  iccpnfhmeo  18459  xrhmeo  18460  iundisj2  18922  reefiso  19840  recosf1o  19913  isabloi  20971  issubgoi  20993  exidu1  21009  rngoideu  21067  cncph  21413  hvsubf  21611  hhip  21772  hhph  21773  helch  21839  hsn0elch  21843  hhshsslem2  21861  shscli  21912  shintcli  21924  pjmf1  22311  idunop  22574  idhmop  22578  0hmop  22579  adj0  22590  lnopunii  22608  lnophmi  22614  riesz4i  22659  cnlnadjlem9  22671  adjcoi  22696  bra11  22704  pjhmopi  22742  iistmd  23301  cnre2csqima  23310  mndpluscn  23314  raddcn  23317  xrge0iifmhm  23336  xrge0pluscn  23337  iundisj2fi  23379  iundisj2f  23381  br2base  23589  indispcon  23780  iooscon  23793  ghomsn  24010  soseq  24325  zintdom  25541  hmeogrpi  25639  1ded  25841  mzpclall  26908  kelac2lem  27265  isopiN  29993  isomliN  30051  idlaut  30907
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-cleq 2289  df-clel 2292  df-ral 2561
  Copyright terms: Public domain W3C validator