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

Theorem rgen2a 2868
Description: Generalization rule for restricted quantification. Note that  x and  y needn't be distinct (and illustrates the use of dvelim 2063). (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 2513 . . . . . 6  |-  ( z  =  x  ->  (
z  e.  A  <->  x  e.  A ) )
21dvelimv 2064 . . . . 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 434 . . . . . 6  |-  ( x  e.  A  ->  (
y  e.  A  ->  ph ) )
54alimi 1618 . . . . 5  |-  ( A. y  x  e.  A  ->  A. y ( y  e.  A  ->  ph )
)
62, 5syl6com 35 . . . 4  |-  ( x  e.  A  ->  ( -.  A. y  y  =  x  ->  A. y
( y  e.  A  ->  ph ) ) )
7 eleq1 2513 . . . . . . 7  |-  ( y  =  x  ->  (
y  e.  A  <->  x  e.  A ) )
87biimpd 207 . . . . . 6  |-  ( y  =  x  ->  (
y  e.  A  ->  x  e.  A )
)
98, 4syli 37 . . . . 5  |-  ( y  =  x  ->  (
y  e.  A  ->  ph ) )
109alimi 1618 . . . 4  |-  ( A. y  y  =  x  ->  A. y ( y  e.  A  ->  ph )
)
116, 10pm2.61d2 160 . . 3  |-  ( x  e.  A  ->  A. y
( y  e.  A  ->  ph ) )
12 df-ral 2796 . . 3  |-  ( A. y  e.  A  ph  <->  A. y
( y  e.  A  ->  ph ) )
1311, 12sylibr 212 . 2  |-  ( x  e.  A  ->  A. y  e.  A  ph )
1413rgen 2801 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 1379    e. wcel 1802   A.wral 2791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1598  df-nf 1602  df-cleq 2433  df-clel 2436  df-ral 2796
This theorem is referenced by:  sosn  5056  isoid  6207  f1owe  6231  ordon  6600  fnwelem  6897  issmo  7018  oawordeulem  7202  ecopover  7414  unfilem2  7784  dffi2  7882  inficl  7884  fipwuni  7885  fisn  7886  dffi3  7890  cantnfvalf  8084  r111  8193  alephf1  8466  alephiso  8479  dfac5lem4  8507  kmlem9  8538  ackbij1lem17  8616  fin1a2lem2  8781  fin1a2lem4  8783  axcc2lem  8816  nqereu  9307  addpqf  9322  mulpqf  9324  genpdm  9380  axaddf  9522  axmulf  9523  subf  9824  mulnzcnopr  10198  negiso  10522  cnref1o  11221  xaddf  11429  xmulf  11470  ioof  11628  om2uzf1oi  12040  om2uzisoi  12041  wwlktovf1  12871  reeff1  13729  divalglem9  13933  bitsf1  13970  gcdf  14031  eucalgf  14086  qredeu  14122  1arith  14319  vdwapf  14364  catideu  14946  sscres  15066  fpwipodrs  15665  letsr  15728  mgmidmo  15757  frmdplusg  15893  nmznsg  16116  efgred  16637  isabli  16683  brric  17264  xrsmgm  18324  xrs1cmn  18329  xrge0subm  18330  xrsds  18332  cnsubmlem  18337  cnsubrglem  18339  nn0srg  18357  rge0srg  18358  fibas  19349  fctop  19375  cctop  19377  iccordt  19585  fsubbas  20238  zfbas  20267  ismeti  20698  dscmet  20963  qtopbaslem  21135  tgqioo  21175  xrsxmet  21184  xrsdsre  21185  retopcon  21204  iccconn  21205  iimulcn  21308  icopnfhmeo  21313  iccpnfhmeo  21315  xrhmeo  21316  iundisj2  21829  reefiso  22712  recosf1o  22791  rzgrp  22810  ercgrg  23777  isabloi  25159  issubgoi  25181  exidu1  25197  rngoideu  25255  cncph  25603  hvsubf  25801  hhip  25963  hhph  25964  helch  26030  hsn0elch  26035  hhshsslem2  26053  shscli  26104  shintcli  26116  pjmf1  26503  idunop  26766  idhmop  26770  0hmop  26771  adj0  26782  lnopunii  26800  lnophmi  26806  riesz4i  26851  cnlnadjlem9  26863  adjcoi  26888  bra11  26896  pjhmopi  26934  iundisj2f  27318  iundisj2fi  27471  xrstos  27537  xrge0omnd  27571  reofld  27700  xrge0slmod  27704  iistmd  27754  cnre2csqima  27763  mndpluscn  27778  raddcn  27781  xrge0iifiso  27787  xrge0iifmhm  27791  xrge0pluscn  27792  br2base  28110  sxbrsiga  28131  signswmnd  28384  indispcon  28549  iooscon  28562  ghomsn  28898  soseq  29306  mzpclall  30631  kelac2lem  30982  plusfreseq  32298  nnsgrpmgm  32341  nnsgrp  32342  2zrngamgm  32452  2zrngmmgm  32459  isomliN  34687  idlaut  35543
  Copyright terms: Public domain W3C validator