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

Theorem rgen2a 2803
Description: Generalization rule for restricted quantification. Note that  x and  y needn't be distinct (and illustrates the use of dvelim 2029). (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 2503 . . . . . . . 8  |-  ( y  =  x  ->  (
y  e.  A  <->  x  e.  A ) )
2 rgen2a.1 . . . . . . . . 9  |-  ( ( x  e.  A  /\  y  e.  A )  ->  ph )
32ex 434 . . . . . . . 8  |-  ( x  e.  A  ->  (
y  e.  A  ->  ph ) )
41, 3syl6bi 228 . . . . . . 7  |-  ( y  =  x  ->  (
y  e.  A  -> 
( y  e.  A  ->  ph ) ) )
54pm2.43d 48 . . . . . 6  |-  ( y  =  x  ->  (
y  e.  A  ->  ph ) )
65alimi 1604 . . . . 5  |-  ( A. y  y  =  x  ->  A. y ( y  e.  A  ->  ph )
)
76a1d 25 . . . 4  |-  ( A. y  y  =  x  ->  ( x  e.  A  ->  A. y ( y  e.  A  ->  ph )
) )
8 eleq1 2503 . . . . . 6  |-  ( z  =  x  ->  (
z  e.  A  <->  x  e.  A ) )
98dvelimv 2030 . . . . 5  |-  ( -. 
A. y  y  =  x  ->  ( x  e.  A  ->  A. y  x  e.  A )
)
103alimi 1604 . . . . 5  |-  ( A. y  x  e.  A  ->  A. y ( y  e.  A  ->  ph )
)
119, 10syl6 33 . . . 4  |-  ( -. 
A. y  y  =  x  ->  ( x  e.  A  ->  A. y
( y  e.  A  ->  ph ) ) )
127, 11pm2.61i 164 . . 3  |-  ( x  e.  A  ->  A. y
( y  e.  A  ->  ph ) )
13 df-ral 2741 . . 3  |-  ( A. y  e.  A  ph  <->  A. y
( y  e.  A  ->  ph ) )
1412, 13sylibr 212 . 2  |-  ( x  e.  A  ->  A. y  e.  A  ph )
1514rgen 2802 1  |-  A. x  e.  A  A. y  e.  A  ph
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369   A.wal 1367    e. wcel 1756   A.wral 2736
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-cleq 2436  df-clel 2439  df-ral 2741
This theorem is referenced by:  sosn  4929  isoid  6041  f1owe  6065  ordon  6415  fnwelem  6708  issmo  6830  oawordeulem  7014  ecopover  7225  unfilem2  7598  dffi2  7694  inficl  7696  fipwuni  7697  fisn  7698  dffi3  7702  cantnfvalf  7894  r111  8003  alephf1  8276  alephiso  8289  dfac5lem4  8317  kmlem9  8348  ackbij1lem17  8426  fin1a2lem2  8591  fin1a2lem4  8593  axcc2lem  8626  nqereu  9119  addpqf  9134  mulpqf  9136  genpdm  9192  axaddf  9333  axmulf  9334  subf  9633  mulnzcnopr  10003  negiso  10327  cnref1o  11007  xaddf  11215  xmulf  11256  ioof  11408  om2uzf1oi  11797  om2uzisoi  11798  reeff1  13425  divalglem9  13626  bitsf1  13663  gcdf  13724  eucalgf  13779  qredeu  13814  1arith  14009  vdwapf  14054  catideu  14634  sscres  14757  fpwipodrs  15355  letsr  15418  mgmidmo  15439  frmdplusg  15553  nmznsg  15746  efgred  16266  isabli  16312  xrs1cmn  17875  xrge0subm  17876  xrsds  17878  cnsubmlem  17883  cnsubrglem  17885  fibas  18604  fctop  18630  cctop  18632  iccordt  18840  fsubbas  19462  zfbas  19491  ismeti  19922  dscmet  20187  qtopbaslem  20359  tgqioo  20399  xrsxmet  20408  xrsdsre  20409  retopcon  20428  iccconn  20429  iimulcn  20532  icopnfhmeo  20537  iccpnfhmeo  20539  xrhmeo  20540  iundisj2  21052  reefiso  21935  recosf1o  22013  isabloi  23797  issubgoi  23819  exidu1  23835  rngoideu  23893  cncph  24241  hvsubf  24439  hhip  24601  hhph  24602  helch  24668  hsn0elch  24673  hhshsslem2  24691  shscli  24742  shintcli  24754  pjmf1  25141  idunop  25404  idhmop  25408  0hmop  25409  adj0  25420  lnopunii  25438  lnophmi  25444  riesz4i  25489  cnlnadjlem9  25501  adjcoi  25526  bra11  25534  pjhmopi  25572  iundisj2f  25954  iundisj2fi  26103  xrstos  26162  xrge0omnd  26196  reofld  26330  xrge0slmod  26334  iistmd  26354  cnre2csqima  26363  mndpluscn  26378  raddcn  26381  xrge0iifiso  26387  xrge0iifmhm  26391  xrge0pluscn  26392  br2base  26706  sxbrsiga  26727  indispcon  27145  iooscon  27158  ghomsn  27329  soseq  27737  mzpclall  29089  kelac2lem  29443  wwlktovf1  30278  isomliN  32980  idlaut  33836
  Copyright terms: Public domain W3C validator