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

Theorem rgen2a 2884
Description: Generalization rule for restricted quantification. Note that and needn't be distinct (and illustrates the use of dvelim 2079). (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
Assertion
Ref Expression
rgen2a
Distinct variable group:   ,

Proof of Theorem rgen2a
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 eleq1 2529 . . . . . 6
21dvelimv 2080 . . . . 5
3 rgen2a.1 . . . . . . 7
43ex 434 . . . . . 6
54alimi 1633 . . . . 5
62, 5syl6com 35 . . . 4
7 eleq1 2529 . . . . . . 7
87biimpd 207 . . . . . 6
98, 4syli 37 . . . . 5
109alimi 1633 . . . 4
116, 10pm2.61d2 160 . . 3
12 df-ral 2812 . . 3
1311, 12sylibr 212 . 2
1413rgen 2817 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  /\wa 369  A.wal 1393  e.wcel 1818  A.wral 2807
This theorem is referenced by:  sosn  5074  isoid  6225  f1owe  6249  ordon  6618  fnwelem  6915  issmo  7038  oawordeulem  7222  ecopover  7434  unfilem2  7805  dffi2  7903  inficl  7905  fipwuni  7906  fisn  7907  dffi3  7911  cantnfvalf  8105  r111  8214  alephf1  8487  alephiso  8500  dfac5lem4  8528  kmlem9  8559  ackbij1lem17  8637  fin1a2lem2  8802  fin1a2lem4  8804  axcc2lem  8837  nqereu  9328  addpqf  9343  mulpqf  9345  genpdm  9401  axaddf  9543  axmulf  9544  subf  9845  mulnzcnopr  10220  negiso  10544  cnref1o  11244  xaddf  11452  xmulf  11493  ioof  11651  om2uzf1oi  12064  om2uzisoi  12065  wwlktovf1  12895  reeff1  13855  divalglem9  14059  bitsf1  14096  gcdf  14157  eucalgf  14212  qredeu  14248  1arith  14445  vdwapf  14490  catideu  15072  sscres  15192  fpwipodrs  15794  letsr  15857  mgmidmo  15886  frmdplusg  16022  nmznsg  16245  efgred  16766  isabli  16812  brric  17393  xrsmgm  18453  xrs1cmn  18458  xrge0subm  18459  xrsds  18461  cnsubmlem  18466  cnsubrglem  18468  nn0srg  18486  rge0srg  18487  fibas  19479  fctop  19505  cctop  19507  iccordt  19715  fsubbas  20368  zfbas  20397  ismeti  20828  dscmet  21093  qtopbaslem  21265  tgqioo  21305  xrsxmet  21314  xrsdsre  21315  retopcon  21334  iccconn  21335  iimulcn  21438  icopnfhmeo  21443  iccpnfhmeo  21445  xrhmeo  21446  iundisj2  21959  reefiso  22843  recosf1o  22922  rzgrp  22941  ercgrg  23908  isabloi  25290  issubgoi  25312  exidu1  25328  rngoideu  25386  cncph  25734  hvsubf  25932  hhip  26094  hhph  26095  helch  26161  hsn0elch  26166  hhshsslem2  26184  shscli  26235  shintcli  26247  pjmf1  26634  idunop  26897  idhmop  26901  0hmop  26902  adj0  26913  lnopunii  26931  lnophmi  26937  riesz4i  26982  cnlnadjlem9  26994  adjcoi  27019  bra11  27027  pjhmopi  27065  iundisj2f  27449  iundisj2fi  27602  xrstos  27667  xrge0omnd  27701  reofld  27830  xrge0slmod  27834  iistmd  27884  cnre2csqima  27893  mndpluscn  27908  raddcn  27911  xrge0iifiso  27917  xrge0iifmhm  27921  xrge0pluscn  27922  br2base  28240  sxbrsiga  28261  signswmnd  28514  indispcon  28679  iooscon  28692  ghomsn  29028  soseq  29334  mzpclall  30659  kelac2lem  31010  plusfreseq  32460  nnsgrpmgm  32504  nnsgrp  32505  2zrngamgm  32745  2zrngmmgm  32752  isomliN  34964  idlaut  35820
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-nf 1617  df-cleq 2449  df-clel 2452  df-ral 2812
  Copyright terms: Public domain W3C validator