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

Theorem rgen2a 2859
Description: Generalization rule for restricted quantification. Note that  x and  y needn't be distinct (and illustrates the use of dvelim 2135). (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 2501 . . . . . 6  |-  ( z  =  x  ->  (
z  e.  A  <->  x  e.  A ) )
21dvelimv 2136 . . . . 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 435 . . . . . 6  |-  ( x  e.  A  ->  (
y  e.  A  ->  ph ) )
54alimi 1680 . . . . 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 2501 . . . . . . 7  |-  ( y  =  x  ->  (
y  e.  A  <->  x  e.  A ) )
87biimpd 210 . . . . . 6  |-  ( y  =  x  ->  (
y  e.  A  ->  x  e.  A )
)
98, 4syli 38 . . . . 5  |-  ( y  =  x  ->  (
y  e.  A  ->  ph ) )
109alimi 1680 . . . 4  |-  ( A. y  y  =  x  ->  A. y ( y  e.  A  ->  ph )
)
116, 10pm2.61d2 163 . . 3  |-  ( x  e.  A  ->  A. y
( y  e.  A  ->  ph ) )
12 df-ral 2787 . . 3  |-  ( A. y  e.  A  ph  <->  A. y
( y  e.  A  ->  ph ) )
1311, 12sylibr 215 . 2  |-  ( x  e.  A  ->  A. y  e.  A  ph )
1413rgen 2792 1  |-  A. x  e.  A  A. y  e.  A  ph
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 370   A.wal 1435    e. wcel 1870   A.wral 2782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-nf 1664  df-cleq 2421  df-clel 2424  df-ral 2787
This theorem is referenced by:  sosn  4924  isoid  6235  f1owe  6259  ordon  6623  fnwelem  6922  issmo  7075  oawordeulem  7263  ecopover  7475  unfilem2  7842  dffi2  7943  inficl  7945  fipwuni  7946  fisn  7947  dffi3  7951  cantnfvalf  8169  r111  8245  alephf1  8514  alephiso  8527  dfac5lem4  8555  kmlem9  8586  ackbij1lem17  8664  fin1a2lem2  8829  fin1a2lem4  8831  axcc2lem  8864  nqereu  9353  addpqf  9368  mulpqf  9370  genpdm  9426  axaddf  9568  axmulf  9569  subf  9876  mulnzcnopr  10257  negiso  10587  cnref1o  11297  xaddf  11517  xmulf  11558  ioof  11732  om2uzf1oi  12164  om2uzisoi  12165  wwlktovf1  13011  reeff1  14152  divalglem9  14357  bitsf1  14394  gcdf  14457  eucalgf  14513  qredeu  14626  1arith  14825  vdwapf  14876  catideu  15523  sscres  15670  fpwipodrs  16352  letsr  16415  mgmidmo  16444  frmdplusg  16580  nmznsg  16803  efgred  17324  isabli  17370  brric  17898  xrsmgm  18929  xrs1cmn  18934  xrge0subm  18935  xrsds  18937  cnsubmlem  18942  cnsubrglem  18944  nn0srg  18962  rge0srg  18963  fibas  19915  fctop  19941  cctop  19943  iccordt  20152  fsubbas  20804  zfbas  20833  ismeti  21262  dscmet  21509  qtopbaslem  21681  tgqioo  21720  xrsxmet  21729  xrsdsre  21730  retopcon  21749  iccconn  21750  iimulcn  21853  icopnfhmeo  21858  iccpnfhmeo  21860  xrhmeo  21861  iundisj2  22370  reefiso  23259  recosf1o  23340  rzgrp  23359  ercgrg  24415  isabloi  25852  issubgoi  25874  exidu1  25890  rngoideu  25948  cncph  26296  hvsubf  26494  hhip  26656  hhph  26657  helch  26722  hsn0elch  26727  hhshsslem2  26745  shscli  26796  shintcli  26808  pjmf1  27195  idunop  27457  idhmop  27461  0hmop  27462  adj0  27473  lnopunii  27491  lnophmi  27497  riesz4i  27542  cnlnadjlem9  27554  adjcoi  27579  bra11  27587  pjhmopi  27625  iundisj2f  28030  iundisj2fi  28200  xrstos  28269  xrge0omnd  28303  reofld  28433  xrge0slmod  28437  iistmd  28538  cnre2csqima  28547  mndpluscn  28562  raddcn  28565  xrge0iifiso  28571  xrge0iifmhm  28575  xrge0pluscn  28576  br2base  28921  sxbrsiga  28942  signswmnd  29225  indispcon  29736  iooscon  29749  ghomsn  30085  soseq  30270  f1omptsnlem  31463  isbasisrelowl  31486  poimirlem27  31661  isomliN  32504  idlaut  33360  mzpclall  35268  kelac2lem  35618  plusfreseq  38520  nnsgrpmgm  38564  nnsgrp  38565  2zrngamgm  38687  2zrngmmgm  38694
  Copyright terms: Public domain W3C validator