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

Theorem rgen2a 2827
Description: Generalization rule for restricted quantification. Note that  x and  y needn't be distinct (and illustrates the use of dvelim 2182). (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 2528 . . . . . 6  |-  ( z  =  x  ->  (
z  e.  A  <->  x  e.  A ) )
21dvelimv 2183 . . . . 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 440 . . . . . 6  |-  ( x  e.  A  ->  (
y  e.  A  ->  ph ) )
54alimi 1695 . . . . 5  |-  ( A. y  x  e.  A  ->  A. y ( y  e.  A  ->  ph )
)
62, 5syl6com 36 . . . 4  |-  ( x  e.  A  ->  ( -.  A. y  y  =  x  ->  A. y
( y  e.  A  ->  ph ) ) )
7 eleq1 2528 . . . . . . 7  |-  ( y  =  x  ->  (
y  e.  A  <->  x  e.  A ) )
87biimpd 212 . . . . . 6  |-  ( y  =  x  ->  (
y  e.  A  ->  x  e.  A )
)
98, 4syli 38 . . . . 5  |-  ( y  =  x  ->  (
y  e.  A  ->  ph ) )
109alimi 1695 . . . 4  |-  ( A. y  y  =  x  ->  A. y ( y  e.  A  ->  ph )
)
116, 10pm2.61d2 165 . . 3  |-  ( x  e.  A  ->  A. y
( y  e.  A  ->  ph ) )
12 df-ral 2754 . . 3  |-  ( A. y  e.  A  ph  <->  A. y
( y  e.  A  ->  ph ) )
1311, 12sylibr 217 . 2  |-  ( x  e.  A  ->  A. y  e.  A  ph )
1413rgen 2759 1  |-  A. x  e.  A  A. y  e.  A  ph
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 375   A.wal 1453    e. wcel 1898   A.wral 2749
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675  df-nf 1679  df-cleq 2455  df-clel 2458  df-ral 2754
This theorem is referenced by:  sosn  4926  isoid  6250  f1owe  6274  ordon  6641  fnwelem  6943  issmo  7098  oawordeulem  7286  ecopover  7498  unfilem2  7867  dffi2  7968  inficl  7970  fipwuni  7971  fisn  7972  dffi3  7976  cantnfvalf  8201  r111  8277  alephf1  8547  alephiso  8560  dfac5lem4  8588  kmlem9  8619  ackbij1lem17  8697  fin1a2lem2  8862  fin1a2lem4  8864  axcc2lem  8897  nqereu  9385  addpqf  9400  mulpqf  9402  genpdm  9458  axaddf  9600  axmulf  9601  subf  9908  mulnzcnopr  10291  negiso  10620  cnref1o  11331  xaddf  11551  xmulf  11592  ioof  11766  om2uzf1oi  12205  om2uzisoi  12206  wwlktovf1  13087  reeff1  14229  divalglem9  14436  divalglem9OLD  14437  bitsf1  14475  gcdf  14538  eucalgf  14597  qredeu  14719  1arith  14926  vdwapf  14977  catideu  15636  sscres  15783  fpwipodrs  16465  letsr  16528  mgmidmo  16557  frmdplusg  16693  nmznsg  16916  efgred  17453  isabli  17499  brric  18027  xrsmgm  19058  xrs1cmn  19063  xrge0subm  19064  xrsds  19066  cnsubmlem  19071  cnsubrglem  19073  nn0srg  19092  rge0srg  19093  fibas  20048  fctop  20074  cctop  20076  iccordt  20285  fsubbas  20937  zfbas  20966  ismeti  21395  dscmet  21642  qtopbaslem  21834  tgqioo  21873  xrsxmet  21882  xrsdsre  21883  retopcon  21902  iccconn  21903  iimulcn  22021  icopnfhmeo  22026  iccpnfhmeo  22028  xrhmeo  22029  iundisj2  22558  reefiso  23459  recosf1o  23540  rzgrp  23559  ercgrg  24618  isabloi  26072  issubgoi  26094  exidu1  26110  rngoideu  26168  cncph  26516  hvsubf  26724  hhip  26886  hhph  26887  helch  26952  hsn0elch  26957  hhshsslem2  26975  shscli  27026  shintcli  27038  pjmf1  27425  idunop  27687  idhmop  27691  0hmop  27692  adj0  27703  lnopunii  27721  lnophmi  27727  riesz4i  27772  cnlnadjlem9  27784  adjcoi  27809  bra11  27817  pjhmopi  27855  iundisj2f  28254  iundisj2fi  28425  xrstos  28493  xrge0omnd  28525  reofld  28654  xrge0slmod  28658  iistmd  28759  cnre2csqima  28768  mndpluscn  28783  raddcn  28786  xrge0iifiso  28792  xrge0iifmhm  28796  xrge0pluscn  28797  br2base  29141  sxbrsiga  29162  signswmnd  29496  indispcon  30007  iooscon  30020  ghomsn  30356  soseq  30542  f1omptsnlem  31784  isbasisrelowl  31807  poimirlem27  32013  isomliN  32851  idlaut  33707  mzpclall  35615  kelac2lem  35968  icof  37557  plusfreseq  40141  nnsgrpmgm  40185  nnsgrp  40186  2zrngamgm  40308  2zrngmmgm  40315
  Copyright terms: Public domain W3C validator