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

Theorem rgen 2608
Description: Generalization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
Hypothesis
Ref Expression
rgen.1  |-  ( x  e.  A  ->  ph )
Assertion
Ref Expression
rgen  |-  A. x  e.  A  ph

Proof of Theorem rgen
StepHypRef Expression
1 df-ral 2548 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 rgen.1 . 2  |-  ( x  e.  A  ->  ph )
31, 2mpgbir 1537 1  |-  A. x  e.  A  ph
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   A.wral 2543
This theorem is referenced by:  rgen2a  2609  rgenw  2610  mprg  2612  mprgbir  2613  rgen2  2639  r19.21be  2644  nrex  2645  rexlimi  2660  sbcth2  3074  reuss  3449  r19.2zb  3544  ral0  3558  unimax  3861  mpteq1  4100  mpteq2ia  4102  reusv2lem4  4538  onssmin  4588  tfis  4645  omssnlim  4670  finds  4682  finds2  4684  fnopab  5368  fmpti  5683  opabex3  5769  sorpssuni  6286  sorpssint  6287  seqomlem2  6463  findcard3  7100  fifo  7185  fisupcl  7218  dfom3  7348  cantnfvalf  7366  rankf  7466  scottex  7555  cplem1  7559  harcard  7611  cardiun  7615  r0weon  7640  acnnum  7679  alephon  7696  alephsmo  7729  alephf1ALT  7730  alephfplem4  7734  dfac5lem4  7753  dfacacn  7767  kmlem1  7776  cflem  7872  cflecard  7879  cfsmolem  7896  fin23lem17  7964  hsmexlem4  8055  omina  8313  0tsk  8377  inar1  8397  wfgru  8438  reclem2pr  8672  nnssre  9750  dfnn2  9759  dfnn3  9760  nnind  9764  nnsub  9784  dfuzi  10102  uzinfmi  10297  uzsupss  10310  cnref1o  10349  xrsupsslem  10625  xrinfmsslem  10626  xrsup0  10642  ser0f  11099  bccl  11334  hashkf  11339  hashbc  11391  wrdind  11477  sqrlem5  11732  rexuz3  11832  sqrf  11847  ackbijnn  12286  incexclem  12295  eff2  12379  reeff1  12400  sqr2irr  12527  prmind2  12769  3prm  12775  pockthi  12954  infpn2  12960  prminf  12962  prmreclem2  12964  prmrec  12969  1arith  12974  1arith2  12975  vdwlem13  13040  ramz  13072  prmlem1a  13108  xpsff1o  13470  isacs1i  13559  dmaf  13881  cdaf  13882  dmcoass  13898  coapm  13903  lubid  14116  odf  14852  efgrelexlemb  15059  dprd2da  15277  mgpf  15352  prdscrngd  15396  cnfld1  16399  cnsubglem  16420  cnmsubglem  16434  isbasis3g  16687  basdif0  16691  distop  16733  mretopd  16829  2ndcsep  17185  kqf  17438  fbssfi  17532  filcon  17578  prdstmdd  17806  prdsxmslem2  18075  qdensere  18279  recld2  18320  ovolf  18841  dyadmax  18953  dveflem  19326  mdegxrf  19454  fta1  19688  vieta1  19692  aalioulem2  19713  taylfval  19738  pilem2  19828  pilem3  19829  recosf1o  19897  divlogrlim  19982  logcn  19994  ressatans  20230  leibpi  20238  ftalem3  20312  chtub  20451  2sqlem6  20608  2sqlem10  20613  chtppilim  20624  pntpbnd1  20735  pntlem3  20758  padicabvf  20780  isgrpoi  20865  cnid  21018  mulid  21023  cnrngo  21070  isvci  21138  isnvi  21169  ipasslem8  21415  hilid  21740  hlimf  21817  shsspwh  21825  pjrni  22281  pjmf1  22295  df0op2  22332  dfiop2  22333  hoaddcomi  22352  hoaddassi  22356  hocadddiri  22359  hocsubdiri  22360  hoaddid1i  22366  ho0coi  22368  hoid1i  22369  hoid1ri  22370  honegsubi  22376  hoddii  22569  lnopunilem2  22591  elunop2  22593  lnophm  22599  imaelshi  22638  cnlnadjlem8  22654  pjnmopi  22728  pjsdii  22735  pjddii  22736  pjtoi  22759  chirred  22975  ballotlem7  23094  dmvlsiga  23490  dya2iocct  23581  indval2  23598  coinfliprv  23683  kur14lem9  23745  dfon2lem7  24145  epsetlike  24194  wfisg  24209  frinsg  24245  wfr3  24275  bdayfo  24329  nodense  24343  fobigcup  24440  axcontlem2  24593  onsucsuccmpi  24882  domncnt  25282  ranncnt  25283  prodeq123i  25317  basexre  25522  intopcoaconlem3  25539  intopcoaconb  25540  intopcoaconc  25541  usptop  25550  1ded  25738  0ded  25757  0catOLD  25758  smbkle  26043  fnckle  26045  pfsubkl  26047  iscola2  26092  nn0prpwlem  26238  refref  26285  topmeet  26313  indexa  26412  sstotbnd2  26498  heiborlem7  26541  mzpclall  26805  dgraaf  27352  phisum  27518  clim1fr1  27727  stoweidlem57  27806  wallispilem3  27816  wallispilem5  27818  wallispi  27819  stirlinglem5  27827  stirlinglem13  27835  stirlinglem14  27836  stirlinglem15  27837  stirlingr  27839  bnj580  28945  bnj1384  29062  bnj1497  29090  isatliN  29492  atpsubN  29942  idldil  30303  cdleme50ldil  30737
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533
This theorem depends on definitions:  df-bi 177  df-ral 2548
  Copyright terms: Public domain W3C validator