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

Theorem rgen 2772
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 2711 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 rgen.1 . 2  |-  ( x  e.  A  ->  ph )
31, 2mpgbir 1560 1  |-  A. x  e.  A  ph
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726   A.wral 2706
This theorem is referenced by:  rgen2a  2773  rgenw  2774  mprg  2776  mprgbir  2777  rgen2  2803  r19.21be  2808  nrex  2809  rexlimi  2824  sbcth2  3245  reuss  3623  r19.2zb  3719  ral0  3733  unimax  4050  mpteq1  4290  mpteq2ia  4292  reusv2lem4  4728  onssmin  4778  tfis  4835  omssnlim  4860  finds  4872  finds2  4874  fnopab  5570  fmpti  5893  opabex3  5991  sorpssuni  6532  sorpssint  6533  seqomlem2  6709  findcard3  7351  fifo  7438  fisupcl  7473  dfom3  7603  cantnfvalf  7621  rankf  7721  scottex  7810  cplem1  7814  harcard  7866  cardiun  7870  r0weon  7895  acnnum  7934  alephon  7951  alephsmo  7984  alephf1ALT  7985  alephfplem4  7989  dfac5lem4  8008  dfacacn  8022  kmlem1  8031  cflem  8127  cflecard  8134  cfsmolem  8151  fin23lem17  8219  hsmexlem4  8310  omina  8567  0tsk  8631  inar1  8651  wfgru  8692  reclem2pr  8926  nnssre  10005  dfnn2  10014  dfnn3  10015  nnind  10019  nnsub  10039  dfuzi  10361  uzinfmi  10556  uzsupss  10569  cnref1o  10608  xrsupsslem  10886  xrinfmsslem  10887  xrsup0  10903  ser0f  11377  bccl  11614  hashkf  11621  hashbc  11703  wrdind  11792  sqrlem5  12053  rexuz3  12153  sqrf  12168  ackbijnn  12608  incexclem  12617  eff2  12701  reeff1  12722  sqr2irr  12849  prmind2  13091  3prm  13097  pockthi  13276  infpn2  13282  prminf  13284  prmreclem2  13286  prmrec  13291  1arith  13296  1arith2  13297  vdwlem13  13362  ramz  13394  prmlem1a  13430  xpsff1o  13794  isacs1i  13883  dmaf  14205  cdaf  14206  coapm  14227  lubid  14440  odf  15176  efgrelexlemb  15383  dprd2da  15601  mgpf  15676  prdscrngd  15720  cnfld1  16727  cnsubglem  16748  cnmsubglem  16762  isbasis3g  17015  basdif0  17019  distop  17061  mretopd  17157  2ndcsep  17523  kqf  17780  fbssfi  17870  filcon  17916  prdstmdd  18154  ustfilxp  18243  prdsxmslem2  18560  qdensere  18805  recld2  18846  ovolf  19379  dyadmax  19491  dveflem  19864  mdegxrf  19992  fta1  20226  vieta1  20230  aalioulem2  20251  taylfval  20276  pilem2  20369  pilem3  20370  recosf1o  20438  divlogrlim  20527  logcn  20539  ressatans  20775  leibpi  20783  ftalem3  20858  chtub  20997  2sqlem6  21154  2sqlem10  21159  chtppilim  21170  pntpbnd1  21281  pntlem3  21304  padicabvf  21326  isgrpoi  21787  cnid  21940  mulid  21945  cnrngo  21992  isvci  22062  isnvi  22093  ipasslem8  22339  hilid  22664  hlimf  22741  shsspwh  22749  pjrni  23205  pjmf1  23219  df0op2  23256  dfiop2  23257  hoaddcomi  23276  hoaddassi  23280  hocadddiri  23283  hocsubdiri  23284  hoaddid1i  23290  ho0coi  23292  hoid1i  23293  hoid1ri  23294  honegsubi  23300  hoddii  23493  lnopunilem2  23515  elunop2  23517  lnophm  23523  imaelshi  23562  cnlnadjlem8  23578  pjnmopi  23652  pjsdii  23659  pjddii  23660  pjtoi  23683  chirred  23899  cnzh  24355  rezh  24356  dmvlsiga  24513  volmeas  24588  sxbrsigalem3  24623  coinfliprv  24741  ballotlem7  24794  kur14lem9  24901  prodf1f  25221  dfon2lem7  25417  epsetlike  25470  wfisg  25485  frinsg  25521  wfr3  25557  tfrALTlem  25558  bdayfo  25631  nodense  25645  fobigcup  25746  axcontlem2  25905  onsucsuccmpi  26194  mblfinlem1  26244  volsupnfl  26252  itg2addnc  26260  nn0prpwlem  26326  refref  26366  topmeet  26394  indexa  26436  sstotbnd2  26484  heiborlem7  26527  mzpclall  26785  dgraaf  27330  phisum  27496  stoweidlem57  27783  wallispilem3  27793  stirlinglem13  27812  bnj580  29285  bnj1384  29402  bnj1497  29430  isatliN  30101  atpsubN  30551  idldil  30912  cdleme50ldil  31346
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556
This theorem depends on definitions:  df-bi 179  df-ral 2711
  Copyright terms: Public domain W3C validator