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

Theorem rgen 2621
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 2561 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 rgen.1 . 2  |-  ( x  e.  A  ->  ph )
31, 2mpgbir 1540 1  |-  A. x  e.  A  ph
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696   A.wral 2556
This theorem is referenced by:  rgen2a  2622  rgenw  2623  mprg  2625  mprgbir  2626  rgen2  2652  r19.21be  2657  nrex  2658  rexlimi  2673  sbcth2  3087  reuss  3462  r19.2zb  3557  ral0  3571  unimax  3877  mpteq1  4116  mpteq2ia  4118  reusv2lem4  4554  onssmin  4604  tfis  4661  omssnlim  4686  finds  4698  finds2  4700  fnopab  5384  fmpti  5699  opabex3  5785  sorpssuni  6302  sorpssint  6303  seqomlem2  6479  findcard3  7116  fifo  7201  fisupcl  7234  dfom3  7364  cantnfvalf  7382  rankf  7482  scottex  7571  cplem1  7575  harcard  7627  cardiun  7631  r0weon  7656  acnnum  7695  alephon  7712  alephsmo  7745  alephf1ALT  7746  alephfplem4  7750  dfac5lem4  7769  dfacacn  7783  kmlem1  7792  cflem  7888  cflecard  7895  cfsmolem  7912  fin23lem17  7980  hsmexlem4  8071  omina  8329  0tsk  8393  inar1  8413  wfgru  8454  reclem2pr  8688  nnssre  9766  dfnn2  9775  dfnn3  9776  nnind  9780  nnsub  9800  dfuzi  10118  uzinfmi  10313  uzsupss  10326  cnref1o  10365  xrsupsslem  10641  xrinfmsslem  10642  xrsup0  10658  ser0f  11115  bccl  11350  hashkf  11355  hashbc  11407  wrdind  11493  sqrlem5  11748  rexuz3  11848  sqrf  11863  ackbijnn  12302  incexclem  12311  eff2  12395  reeff1  12416  sqr2irr  12543  prmind2  12785  3prm  12791  pockthi  12970  infpn2  12976  prminf  12978  prmreclem2  12980  prmrec  12985  1arith  12990  1arith2  12991  vdwlem13  13056  ramz  13088  prmlem1a  13124  xpsff1o  13486  isacs1i  13575  dmaf  13897  cdaf  13898  dmcoass  13914  coapm  13919  lubid  14132  odf  14868  efgrelexlemb  15075  dprd2da  15293  mgpf  15368  prdscrngd  15412  cnfld1  16415  cnsubglem  16436  cnmsubglem  16450  isbasis3g  16703  basdif0  16707  distop  16749  mretopd  16845  2ndcsep  17201  kqf  17454  fbssfi  17548  filcon  17594  prdstmdd  17822  prdsxmslem2  18091  qdensere  18295  recld2  18336  ovolf  18857  dyadmax  18969  dveflem  19342  mdegxrf  19470  fta1  19704  vieta1  19708  aalioulem2  19729  taylfval  19754  pilem2  19844  pilem3  19845  recosf1o  19913  divlogrlim  19998  logcn  20010  ressatans  20246  leibpi  20254  ftalem3  20328  chtub  20467  2sqlem6  20624  2sqlem10  20629  chtppilim  20640  pntpbnd1  20751  pntlem3  20774  padicabvf  20796  isgrpoi  20881  cnid  21034  mulid  21039  cnrngo  21086  isvci  21154  isnvi  21185  ipasslem8  21431  hilid  21756  hlimf  21833  shsspwh  21841  pjrni  22297  pjmf1  22311  df0op2  22348  dfiop2  22349  hoaddcomi  22368  hoaddassi  22372  hocadddiri  22375  hocsubdiri  22376  hoaddid1i  22382  ho0coi  22384  hoid1i  22385  hoid1ri  22386  honegsubi  22392  hoddii  22585  lnopunilem2  22607  elunop2  22609  lnophm  22615  imaelshi  22654  cnlnadjlem8  22670  pjnmopi  22744  pjsdii  22751  pjddii  22752  pjtoi  22775  chirred  22991  ballotlem7  23110  dmvlsiga  23505  dya2iocct  23596  indval2  23613  coinfliprv  23698  kur14lem9  23760  prodf1f  24166  dfon2lem7  24216  epsetlike  24265  wfisg  24280  frinsg  24316  wfr3  24346  bdayfo  24400  nodense  24414  fobigcup  24511  axcontlem2  24665  onsucsuccmpi  24954  itg2addnc  25005  domncnt  25385  ranncnt  25386  prodeq123i  25420  basexre  25625  intopcoaconlem3  25642  intopcoaconb  25643  intopcoaconc  25644  usptop  25653  1ded  25841  0ded  25860  0catOLD  25861  smbkle  26146  fnckle  26148  pfsubkl  26150  iscola2  26195  nn0prpwlem  26341  refref  26388  topmeet  26416  indexa  26515  sstotbnd2  26601  heiborlem7  26644  mzpclall  26908  dgraaf  27455  phisum  27621  clim1fr1  27830  stoweidlem57  27909  wallispilem3  27919  wallispilem5  27921  wallispi  27922  stirlinglem5  27930  stirlinglem13  27938  stirlinglem14  27939  stirlinglem15  27940  stirlingr  27942  bnj580  29261  bnj1384  29378  bnj1497  29406  isatliN  30114  atpsubN  30564  idldil  30925  cdleme50ldil  31359
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536
This theorem depends on definitions:  df-bi 177  df-ral 2561
  Copyright terms: Public domain W3C validator