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

Theorem rgen2a 2764
Description: Generalization rule for restricted quantification. Note that  x and  y needn't be distinct (and illustrates the use of dvelim 2069). (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 2495 . . . . . . . 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 1568 . . . . 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 2495 . . . . . 6  |-  ( z  =  x  ->  (
z  e.  A  <->  x  e.  A ) )
98dvelimv 2070 . . . . 5  |-  ( -. 
A. y  y  =  x  ->  ( x  e.  A  ->  A. y  x  e.  A )
)
103alimi 1568 . . . . 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 2702 . . 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 2763 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 1549    e. wcel 1725   A.wral 2697
This theorem is referenced by:  ordon  4755  sosn  4939  isoid  6041  f1owe  6065  fnwelem  6453  issmo  6602  oawordeulem  6789  ecopover  7000  unfilem2  7364  dffi2  7420  inficl  7422  fipwuni  7423  fisn  7424  dffi3  7428  cantnfvalf  7612  r111  7693  alephf1  7958  alephiso  7971  dfac5lem4  7999  kmlem9  8030  ackbij1lem17  8108  fin1a2lem2  8273  fin1a2lem4  8275  axcc2lem  8308  nqereu  8798  addpqf  8813  mulpqf  8815  genpdm  8871  axaddf  9012  axmulf  9013  subf  9299  mulnzcnopr  9660  negiso  9976  cnref1o  10599  xaddf  10802  xmulf  10843  ioof  10994  om2uzf1oi  11285  om2uzisoi  11286  reeff1  12713  divalglem9  12913  bitsf1  12950  gcdf  13011  eucalgf  13066  qredeu  13099  1arith  13287  vdwapf  13332  catideu  13892  sscres  14015  islati  14473  fpwipodrs  14582  letsr  14664  mgmidmo  14685  frmdplusg  14791  nmznsg  14976  efgred  15372  isabli  15418  xrs1cmn  16730  xrge0subm  16731  xrsds  16733  cnsubmlem  16738  cnsubrglem  16740  fibas  17034  fctop  17060  cctop  17062  iccordt  17270  fsubbas  17891  zfbas  17920  ismeti  18347  dscmet  18612  qtopbaslem  18784  tgqioo  18823  xrsxmet  18832  xrsdsre  18833  retopcon  18852  iccconn  18853  iimulcn  18955  icopnfhmeo  18960  iccpnfhmeo  18962  xrhmeo  18963  iundisj2  19435  reefiso  20356  recosf1o  20429  isabloi  21868  issubgoi  21890  exidu1  21906  rngoideu  21964  cncph  22312  hvsubf  22510  hhip  22671  hhph  22672  helch  22738  hsn0elch  22742  hhshsslem2  22760  shscli  22811  shintcli  22823  pjmf1  23210  idunop  23473  idhmop  23477  0hmop  23478  adj0  23489  lnopunii  23507  lnophmi  23513  riesz4i  23558  cnlnadjlem9  23570  adjcoi  23595  bra11  23603  pjhmopi  23641  iundisj2f  24022  iundisj2fi  24145  xrstos  24193  reofld  24272  iistmd  24292  cnre2csqima  24301  mndpluscn  24304  raddcn  24307  xrge0iifiso  24313  xrge0iifmhm  24317  xrge0pluscn  24318  br2base  24611  sxbrsiga  24632  indispcon  24913  iooscon  24926  ghomsn  25091  soseq  25521  mzpclall  26775  kelac2lem  27130  isopiN  29916  isomliN  29974  idlaut  30830
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-cleq 2428  df-clel 2431  df-ral 2702
  Copyright terms: Public domain W3C validator