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

Theorem rgen 2739
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 2679 . 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 1721   A.wral 2674
This theorem is referenced by:  rgen2a  2740  rgenw  2741  mprg  2743  mprgbir  2744  rgen2  2770  r19.21be  2775  nrex  2776  rexlimi  2791  sbcth2  3212  reuss  3590  r19.2zb  3686  ral0  3700  unimax  4017  mpteq1  4257  mpteq2ia  4259  reusv2lem4  4694  onssmin  4744  tfis  4801  omssnlim  4826  finds  4838  finds2  4840  fnopab  5536  fmpti  5859  opabex3  5957  sorpssuni  6498  sorpssint  6499  seqomlem2  6675  findcard3  7317  fifo  7403  fisupcl  7436  dfom3  7566  cantnfvalf  7584  rankf  7684  scottex  7773  cplem1  7777  harcard  7829  cardiun  7833  r0weon  7858  acnnum  7897  alephon  7914  alephsmo  7947  alephf1ALT  7948  alephfplem4  7952  dfac5lem4  7971  dfacacn  7985  kmlem1  7994  cflem  8090  cflecard  8097  cfsmolem  8114  fin23lem17  8182  hsmexlem4  8273  omina  8530  0tsk  8594  inar1  8614  wfgru  8655  reclem2pr  8889  nnssre  9968  dfnn2  9977  dfnn3  9978  nnind  9982  nnsub  10002  dfuzi  10324  uzinfmi  10519  uzsupss  10532  cnref1o  10571  xrsupsslem  10849  xrinfmsslem  10850  xrsup0  10866  ser0f  11339  bccl  11576  hashkf  11583  hashbc  11665  wrdind  11754  sqrlem5  12015  rexuz3  12115  sqrf  12130  ackbijnn  12570  incexclem  12579  eff2  12663  reeff1  12684  sqr2irr  12811  prmind2  13053  3prm  13059  pockthi  13238  infpn2  13244  prminf  13246  prmreclem2  13248  prmrec  13253  1arith  13258  1arith2  13259  vdwlem13  13324  ramz  13356  prmlem1a  13392  xpsff1o  13756  isacs1i  13845  dmaf  14167  cdaf  14168  coapm  14189  lubid  14402  odf  15138  efgrelexlemb  15345  dprd2da  15563  mgpf  15638  prdscrngd  15682  cnfld1  16689  cnsubglem  16710  cnmsubglem  16724  isbasis3g  16977  basdif0  16981  distop  17023  mretopd  17119  2ndcsep  17483  kqf  17740  fbssfi  17830  filcon  17876  prdstmdd  18114  ustfilxp  18203  prdsxmslem2  18520  qdensere  18765  recld2  18806  ovolf  19339  dyadmax  19451  dveflem  19824  mdegxrf  19952  fta1  20186  vieta1  20190  aalioulem2  20211  taylfval  20236  pilem2  20329  pilem3  20330  recosf1o  20398  divlogrlim  20487  logcn  20499  ressatans  20735  leibpi  20743  ftalem3  20818  chtub  20957  2sqlem6  21114  2sqlem10  21119  chtppilim  21130  pntpbnd1  21241  pntlem3  21264  padicabvf  21286  isgrpoi  21747  cnid  21900  mulid  21905  cnrngo  21952  isvci  22022  isnvi  22053  ipasslem8  22299  hilid  22624  hlimf  22701  shsspwh  22709  pjrni  23165  pjmf1  23179  df0op2  23216  dfiop2  23217  hoaddcomi  23236  hoaddassi  23240  hocadddiri  23243  hocsubdiri  23244  hoaddid1i  23250  ho0coi  23252  hoid1i  23253  hoid1ri  23254  honegsubi  23260  hoddii  23453  lnopunilem2  23475  elunop2  23477  lnophm  23483  imaelshi  23522  cnlnadjlem8  23538  pjnmopi  23612  pjsdii  23619  pjddii  23620  pjtoi  23643  chirred  23859  cnzh  24315  rezh  24316  dmvlsiga  24473  volmeas  24548  sxbrsigalem3  24583  coinfliprv  24701  ballotlem7  24754  kur14lem9  24861  prodf1f  25181  dfon2lem7  25367  epsetlike  25416  wfisg  25431  frinsg  25467  wfr3  25497  bdayfo  25551  nodense  25565  fobigcup  25662  axcontlem2  25816  onsucsuccmpi  26105  mblfinlem  26151  volsupnfl  26158  itg2addnc  26166  nn0prpwlem  26223  refref  26263  topmeet  26291  indexa  26333  sstotbnd2  26381  heiborlem7  26424  mzpclall  26682  dgraaf  27228  phisum  27394  stoweidlem57  27681  wallispilem3  27691  stirlinglem13  27710  bnj580  29002  bnj1384  29119  bnj1497  29147  isatliN  29797  atpsubN  30247  idldil  30608  cdleme50ldil  31042
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 2679
  Copyright terms: Public domain W3C validator