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

Theorem rgen 2714
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 2654 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 rgen.1 . 2  |-  ( x  e.  A  ->  ph )
31, 2mpgbir 1556 1  |-  A. x  e.  A  ph
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717   A.wral 2649
This theorem is referenced by:  rgen2a  2715  rgenw  2716  mprg  2718  mprgbir  2719  rgen2  2745  r19.21be  2750  nrex  2751  rexlimi  2766  sbcth2  3187  reuss  3565  r19.2zb  3661  ral0  3675  unimax  3991  mpteq1  4230  mpteq2ia  4232  reusv2lem4  4667  onssmin  4717  tfis  4774  omssnlim  4799  finds  4811  finds2  4813  fnopab  5509  fmpti  5831  opabex3  5929  sorpssuni  6467  sorpssint  6468  seqomlem2  6644  findcard3  7286  fifo  7372  fisupcl  7405  dfom3  7535  cantnfvalf  7553  rankf  7653  scottex  7742  cplem1  7746  harcard  7798  cardiun  7802  r0weon  7827  acnnum  7866  alephon  7883  alephsmo  7916  alephf1ALT  7917  alephfplem4  7921  dfac5lem4  7940  dfacacn  7954  kmlem1  7963  cflem  8059  cflecard  8066  cfsmolem  8083  fin23lem17  8151  hsmexlem4  8242  omina  8499  0tsk  8563  inar1  8583  wfgru  8624  reclem2pr  8858  nnssre  9936  dfnn2  9945  dfnn3  9946  nnind  9950  nnsub  9970  dfuzi  10292  uzinfmi  10487  uzsupss  10500  cnref1o  10539  xrsupsslem  10817  xrinfmsslem  10818  xrsup0  10834  ser0f  11303  bccl  11540  hashkf  11547  hashbc  11629  wrdind  11718  sqrlem5  11979  rexuz3  12079  sqrf  12094  ackbijnn  12534  incexclem  12543  eff2  12627  reeff1  12648  sqr2irr  12775  prmind2  13017  3prm  13023  pockthi  13202  infpn2  13208  prminf  13210  prmreclem2  13212  prmrec  13217  1arith  13222  1arith2  13223  vdwlem13  13288  ramz  13320  prmlem1a  13356  xpsff1o  13720  isacs1i  13809  dmaf  14131  cdaf  14132  coapm  14153  lubid  14366  odf  15102  efgrelexlemb  15309  dprd2da  15527  mgpf  15602  prdscrngd  15646  cnfld1  16649  cnsubglem  16670  cnmsubglem  16684  isbasis3g  16937  basdif0  16941  distop  16983  mretopd  17079  2ndcsep  17443  kqf  17700  fbssfi  17790  filcon  17836  prdstmdd  18074  ustfilxp  18163  prdsxmslem2  18449  qdensere  18675  recld2  18716  ovolf  19245  dyadmax  19357  dveflem  19730  mdegxrf  19858  fta1  20092  vieta1  20096  aalioulem2  20117  taylfval  20142  pilem2  20235  pilem3  20236  recosf1o  20304  divlogrlim  20393  logcn  20405  ressatans  20641  leibpi  20649  ftalem3  20724  chtub  20863  2sqlem6  21020  2sqlem10  21025  chtppilim  21036  pntpbnd1  21147  pntlem3  21170  padicabvf  21192  isgrpoi  21634  cnid  21787  mulid  21792  cnrngo  21839  isvci  21909  isnvi  21940  ipasslem8  22186  hilid  22511  hlimf  22588  shsspwh  22596  pjrni  23052  pjmf1  23066  df0op2  23103  dfiop2  23104  hoaddcomi  23123  hoaddassi  23127  hocadddiri  23130  hocsubdiri  23131  hoaddid1i  23137  ho0coi  23139  hoid1i  23140  hoid1ri  23141  honegsubi  23147  hoddii  23340  lnopunilem2  23362  elunop2  23364  lnophm  23370  imaelshi  23409  cnlnadjlem8  23425  pjnmopi  23499  pjsdii  23506  pjddii  23507  pjtoi  23530  chirred  23746  rrhre  24183  dmvlsiga  24308  volmeas  24381  sxbrsigalem3  24416  coinfliprv  24519  ballotlem7  24572  kur14lem9  24679  prodf1f  24999  dfon2lem7  25169  epsetlike  25218  wfisg  25233  frinsg  25269  wfr3  25299  bdayfo  25353  nodense  25367  fobigcup  25464  axcontlem2  25618  onsucsuccmpi  25907  volsupnfl  25956  itg2addnc  25959  nn0prpwlem  26016  refref  26056  topmeet  26084  indexa  26126  sstotbnd2  26174  heiborlem7  26217  mzpclall  26475  dgraaf  27021  phisum  27187  stoweidlem57  27474  wallispilem3  27484  stirlinglem13  27503  bnj580  28622  bnj1384  28739  bnj1497  28767  isatliN  29417  atpsubN  29867  idldil  30228  cdleme50ldil  30662
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552
This theorem depends on definitions:  df-bi 178  df-ral 2654
  Copyright terms: Public domain W3C validator