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

Theorem rgen2a 2849
Description: Generalization rule for restricted quantification. Note that  x and  y needn't be distinct (and illustrates the use of dvelim 2138). (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 2495 . . . . . 6  |-  ( z  =  x  ->  (
z  e.  A  <->  x  e.  A ) )
21dvelimv 2139 . . . . 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 1678 . . . . 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 2495 . . . . . . 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 1678 . . . 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 2776 . . 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 2781 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 1872   A.wral 2771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1658  df-nf 1662  df-cleq 2414  df-clel 2417  df-ral 2776
This theorem is referenced by:  sosn  4923  isoid  6235  f1owe  6259  ordon  6623  fnwelem  6922  issmo  7078  oawordeulem  7266  ecopover  7478  unfilem2  7845  dffi2  7946  inficl  7948  fipwuni  7949  fisn  7950  dffi3  7954  cantnfvalf  8178  r111  8254  alephf1  8523  alephiso  8536  dfac5lem4  8564  kmlem9  8595  ackbij1lem17  8673  fin1a2lem2  8838  fin1a2lem4  8840  axcc2lem  8873  nqereu  9361  addpqf  9376  mulpqf  9378  genpdm  9434  axaddf  9576  axmulf  9577  subf  9884  mulnzcnopr  10265  negiso  10594  cnref1o  11304  xaddf  11524  xmulf  11565  ioof  11739  om2uzf1oi  12173  om2uzisoi  12174  wwlktovf1  13032  reeff1  14173  divalglem9  14380  divalglem9OLD  14381  bitsf1  14419  gcdf  14482  eucalgf  14541  qredeu  14663  1arith  14870  vdwapf  14921  catideu  15580  sscres  15727  fpwipodrs  16409  letsr  16472  mgmidmo  16501  frmdplusg  16637  nmznsg  16860  efgred  17397  isabli  17443  brric  17971  xrsmgm  19002  xrs1cmn  19007  xrge0subm  19008  xrsds  19010  cnsubmlem  19015  cnsubrglem  19017  nn0srg  19035  rge0srg  19036  fibas  19991  fctop  20017  cctop  20019  iccordt  20228  fsubbas  20880  zfbas  20909  ismeti  21338  dscmet  21585  qtopbaslem  21777  tgqioo  21816  xrsxmet  21825  xrsdsre  21826  retopcon  21845  iccconn  21846  iimulcn  21964  icopnfhmeo  21969  iccpnfhmeo  21971  xrhmeo  21972  iundisj2  22500  reefiso  23401  recosf1o  23482  rzgrp  23501  ercgrg  24560  isabloi  26014  issubgoi  26036  exidu1  26052  rngoideu  26110  cncph  26458  hvsubf  26666  hhip  26828  hhph  26829  helch  26894  hsn0elch  26899  hhshsslem2  26917  shscli  26968  shintcli  26980  pjmf1  27367  idunop  27629  idhmop  27633  0hmop  27634  adj0  27645  lnopunii  27663  lnophmi  27669  riesz4i  27714  cnlnadjlem9  27726  adjcoi  27751  bra11  27759  pjhmopi  27797  iundisj2f  28202  iundisj2fi  28379  xrstos  28448  xrge0omnd  28481  reofld  28611  xrge0slmod  28615  iistmd  28716  cnre2csqima  28725  mndpluscn  28740  raddcn  28743  xrge0iifiso  28749  xrge0iifmhm  28753  xrge0pluscn  28754  br2base  29099  sxbrsiga  29120  signswmnd  29454  indispcon  29965  iooscon  29978  ghomsn  30314  soseq  30499  f1omptsnlem  31702  isbasisrelowl  31725  poimirlem27  31931  isomliN  32774  idlaut  33630  mzpclall  35538  kelac2lem  35892  plusfreseq  39392  nnsgrpmgm  39436  nnsgrp  39437  2zrngamgm  39559  2zrngmmgm  39566
  Copyright terms: Public domain W3C validator