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

Theorem rgen2a 2809
Description: Generalization rule for restricted quantification. Note that  x and  y needn't be distinct (and illustrates the use of dvelim 2085). (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 2454 . . . . . 6  |-  ( z  =  x  ->  (
z  e.  A  <->  x  e.  A ) )
21dvelimv 2086 . . . . 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 432 . . . . . 6  |-  ( x  e.  A  ->  (
y  e.  A  ->  ph ) )
54alimi 1641 . . . . 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 2454 . . . . . . 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 1641 . . . 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 2737 . . 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 2742 1  |-  A. x  e.  A  A. y  e.  A  ph
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 367   A.wal 1397    e. wcel 1826   A.wral 2732
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1621  df-nf 1625  df-cleq 2374  df-clel 2377  df-ral 2737
This theorem is referenced by:  sosn  4983  isoid  6126  f1owe  6150  ordon  6517  fnwelem  6814  issmo  6937  oawordeulem  7121  ecopover  7333  unfilem2  7700  dffi2  7798  inficl  7800  fipwuni  7801  fisn  7802  dffi3  7806  cantnfvalf  7997  r111  8106  alephf1  8379  alephiso  8392  dfac5lem4  8420  kmlem9  8451  ackbij1lem17  8529  fin1a2lem2  8694  fin1a2lem4  8696  axcc2lem  8729  nqereu  9218  addpqf  9233  mulpqf  9235  genpdm  9291  axaddf  9433  axmulf  9434  subf  9735  mulnzcnopr  10112  negiso  10435  cnref1o  11134  xaddf  11344  xmulf  11385  ioof  11543  om2uzf1oi  11967  om2uzisoi  11968  wwlktovf1  12806  reeff1  13857  divalglem9  14061  bitsf1  14098  gcdf  14159  eucalgf  14214  qredeu  14250  1arith  14447  vdwapf  14492  catideu  15082  sscres  15229  fpwipodrs  15911  letsr  15974  mgmidmo  16003  frmdplusg  16139  nmznsg  16362  efgred  16883  isabli  16929  brric  17506  xrsmgm  18566  xrs1cmn  18571  xrge0subm  18572  xrsds  18574  cnsubmlem  18579  cnsubrglem  18581  nn0srg  18599  rge0srg  18600  fibas  19564  fctop  19590  cctop  19592  iccordt  19801  fsubbas  20453  zfbas  20482  ismeti  20913  dscmet  21178  qtopbaslem  21350  tgqioo  21390  xrsxmet  21399  xrsdsre  21400  retopcon  21419  iccconn  21420  iimulcn  21523  icopnfhmeo  21528  iccpnfhmeo  21530  xrhmeo  21531  iundisj2  22044  reefiso  22928  recosf1o  23007  rzgrp  23026  ercgrg  24028  isabloi  25407  issubgoi  25429  exidu1  25445  rngoideu  25503  cncph  25851  hvsubf  26049  hhip  26211  hhph  26212  helch  26278  hsn0elch  26283  hhshsslem2  26301  shscli  26352  shintcli  26364  pjmf1  26751  idunop  27013  idhmop  27017  0hmop  27018  adj0  27029  lnopunii  27047  lnophmi  27053  riesz4i  27098  cnlnadjlem9  27110  adjcoi  27135  bra11  27143  pjhmopi  27181  iundisj2f  27579  iundisj2fi  27755  xrstos  27820  xrge0omnd  27854  reofld  27984  xrge0slmod  27988  iistmd  28038  cnre2csqima  28047  mndpluscn  28062  raddcn  28065  xrge0iifiso  28071  xrge0iifmhm  28075  xrge0pluscn  28076  br2base  28396  sxbrsiga  28417  signswmnd  28697  indispcon  28868  iooscon  28881  ghomsn  29217  soseq  29499  mzpclall  30825  kelac2lem  31176  plusfreseq  32778  nnsgrpmgm  32822  nnsgrp  32823  2zrngamgm  32945  2zrngmmgm  32952  isomliN  35377  idlaut  36233
  Copyright terms: Public domain W3C validator