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

Theorem rgen 2763
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 2702 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 rgen.1 . 2  |-  ( x  e.  A  ->  ph )
31, 2mpgbir 1559 1  |-  A. x  e.  A  ph
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   A.wral 2697
This theorem is referenced by:  rgen2a  2764  rgenw  2765  mprg  2767  mprgbir  2768  rgen2  2794  r19.21be  2799  nrex  2800  rexlimi  2815  sbcth2  3236  reuss  3614  r19.2zb  3710  ral0  3724  unimax  4041  mpteq1  4281  mpteq2ia  4283  reusv2lem4  4719  onssmin  4769  tfis  4826  omssnlim  4851  finds  4863  finds2  4865  fnopab  5561  fmpti  5884  opabex3  5982  sorpssuni  6523  sorpssint  6524  seqomlem2  6700  findcard3  7342  fifo  7429  fisupcl  7464  dfom3  7594  cantnfvalf  7612  rankf  7712  scottex  7801  cplem1  7805  harcard  7857  cardiun  7861  r0weon  7886  acnnum  7925  alephon  7942  alephsmo  7975  alephf1ALT  7976  alephfplem4  7980  dfac5lem4  7999  dfacacn  8013  kmlem1  8022  cflem  8118  cflecard  8125  cfsmolem  8142  fin23lem17  8210  hsmexlem4  8301  omina  8558  0tsk  8622  inar1  8642  wfgru  8683  reclem2pr  8917  nnssre  9996  dfnn2  10005  dfnn3  10006  nnind  10010  nnsub  10030  dfuzi  10352  uzinfmi  10547  uzsupss  10560  cnref1o  10599  xrsupsslem  10877  xrinfmsslem  10878  xrsup0  10894  ser0f  11368  bccl  11605  hashkf  11612  hashbc  11694  wrdind  11783  sqrlem5  12044  rexuz3  12144  sqrf  12159  ackbijnn  12599  incexclem  12608  eff2  12692  reeff1  12713  sqr2irr  12840  prmind2  13082  3prm  13088  pockthi  13267  infpn2  13273  prminf  13275  prmreclem2  13277  prmrec  13282  1arith  13287  1arith2  13288  vdwlem13  13353  ramz  13385  prmlem1a  13421  xpsff1o  13785  isacs1i  13874  dmaf  14196  cdaf  14197  coapm  14218  lubid  14431  odf  15167  efgrelexlemb  15374  dprd2da  15592  mgpf  15667  prdscrngd  15711  cnfld1  16718  cnsubglem  16739  cnmsubglem  16753  isbasis3g  17006  basdif0  17010  distop  17052  mretopd  17148  2ndcsep  17514  kqf  17771  fbssfi  17861  filcon  17907  prdstmdd  18145  ustfilxp  18234  prdsxmslem2  18551  qdensere  18796  recld2  18837  ovolf  19370  dyadmax  19482  dveflem  19855  mdegxrf  19983  fta1  20217  vieta1  20221  aalioulem2  20242  taylfval  20267  pilem2  20360  pilem3  20361  recosf1o  20429  divlogrlim  20518  logcn  20530  ressatans  20766  leibpi  20774  ftalem3  20849  chtub  20988  2sqlem6  21145  2sqlem10  21150  chtppilim  21161  pntpbnd1  21272  pntlem3  21295  padicabvf  21317  isgrpoi  21778  cnid  21931  mulid  21936  cnrngo  21983  isvci  22053  isnvi  22084  ipasslem8  22330  hilid  22655  hlimf  22732  shsspwh  22740  pjrni  23196  pjmf1  23210  df0op2  23247  dfiop2  23248  hoaddcomi  23267  hoaddassi  23271  hocadddiri  23274  hocsubdiri  23275  hoaddid1i  23281  ho0coi  23283  hoid1i  23284  hoid1ri  23285  honegsubi  23291  hoddii  23484  lnopunilem2  23506  elunop2  23508  lnophm  23514  imaelshi  23553  cnlnadjlem8  23569  pjnmopi  23643  pjsdii  23650  pjddii  23651  pjtoi  23674  chirred  23890  cnzh  24346  rezh  24347  dmvlsiga  24504  volmeas  24579  sxbrsigalem3  24614  coinfliprv  24732  ballotlem7  24785  kur14lem9  24892  prodf1f  25212  dfon2lem7  25408  epsetlike  25461  wfisg  25476  frinsg  25512  wfr3  25548  tfrALTlem  25549  bdayfo  25622  nodense  25636  fobigcup  25737  axcontlem2  25896  onsucsuccmpi  26185  mblfinlem  26234  volsupnfl  26241  itg2addnc  26249  nn0prpwlem  26306  refref  26346  topmeet  26374  indexa  26416  sstotbnd2  26464  heiborlem7  26507  mzpclall  26765  dgraaf  27310  phisum  27476  stoweidlem57  27763  wallispilem3  27773  stirlinglem13  27792  bnj580  29211  bnj1384  29328  bnj1497  29356  isatliN  30027  atpsubN  30477  idldil  30838  cdleme50ldil  31272
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555
This theorem depends on definitions:  df-bi 178  df-ral 2702
  Copyright terms: Public domain W3C validator