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

Theorem rgen 2951
Description: Generalization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
Hypothesis
Ref Expression
rgen.1 (𝑥𝐴𝜑)
Assertion
Ref Expression
rgen 𝑥𝐴 𝜑

Proof of Theorem rgen
StepHypRef Expression
1 df-ral 2946 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 rgen.1 . 2 (𝑥𝐴𝜑)
31, 2mpgbir 1766 1 𝑥𝐴 𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  wral 2941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762
This theorem depends on definitions:  df-bi 197  df-ral 2946
This theorem is referenced by:  ralel  2952  rgenw  2953  mprg  2955  mprgbir  2956  r19.21be  2962  rgen2  3004  rgen2a  3006  nrex  3029  rexlimi  3053  rexlimiv  3056  sbcth2  3556  r19.2zb  4094  ral0  4109  unimax  4505  mpteq1  4770  mpteq2ia  4773  reusv2lem4  4902  wfisg  5753  fnopab  6056  fmpti  6423  sorpssuni  6988  sorpssint  6989  onssmin  7039  tfis  7096  omssnlim  7121  finds  7134  finds2  7136  opabex3  7188  wfr3  7480  seqomlem2  7591  findcard3  8244  fifo  8379  fisupcl  8416  dfom3  8582  cantnfvalf  8600  rankf  8695  scottex  8786  cplem1  8790  harcard  8842  cardiun  8846  r0weon  8873  acnnum  8913  alephon  8930  alephsmo  8963  alephf1ALT  8964  alephfplem4  8968  dfac5lem4  8987  dfacacn  9001  kmlem1  9010  cflem  9106  cflecard  9113  cfsmolem  9130  fin23lem17  9198  hsmexlem4  9289  omina  9551  0tsk  9615  inar1  9635  wfgru  9676  reclem2pr  9908  nnssre  11062  dfnn2  11071  dfnn3  11072  nnind  11076  nnsub  11097  dfuzi  11506  uzsupss  11818  cnref1o  11865  xrsupsslem  12175  xrinfmsslem  12176  xrsup0  12191  reltre  12208  rpltrp  12209  reltxrnmnf  12210  ser0f  12894  bccl  13149  hashkf  13159  hashbc  13275  wrdind  13522  sqrlem5  14031  rexuz3  14132  sqrtf  14147  ackbijnn  14604  incexclem  14612  prodf1f  14668  eff2  14873  reeff1  14894  sqrt2irr  15023  prmind2  15445  3prm  15453  phisum  15542  pockthi  15658  infpn2  15664  prminf  15666  prmreclem2  15668  prmrec  15673  1arith  15678  1arith2  15679  vdwlem13  15744  ramz  15776  prmgap  15810  prmgaplcm  15811  prmgapprmo  15813  prmlem1a  15860  xpsff1o  16275  isacs1i  16365  dmaf  16746  cdaf  16747  coapm  16768  lublecllem  17035  pmtrdifel  17946  pmtrdifwrdel  17951  odf  18002  efgrelexlemb  18209  dprd2da  18487  mgpf  18605  prdscrngd  18659  cnfld1  19819  cnsubglem  19843  cnmsubglem  19857  nn0srg  19864  rge0srg  19865  pmatcoe1fsupp  20554  isbasis3g  20801  basdif0  20805  distop  20847  mretopd  20944  2ndcsep  21310  refref  21364  kqf  21598  fbssfi  21688  filconn  21734  prdstmdd  21974  ustfilxp  22063  prdsxmslem2  22381  qdensere  22620  recld2  22664  isclmi0  22944  iscvsi  22975  ovolf  23296  dyadmax  23412  dveflem  23787  mdegxrf  23873  fta1  24108  vieta1  24112  aalioulem2  24133  taylfval  24158  pilem2  24251  pilem3  24252  recosf1o  24326  divlogrlim  24426  logcn  24438  ressatans  24706  leibpi  24714  ftalem3  24846  chtub  24982  2sqlem6  25193  2sqlem10  25198  chtppilim  25209  pntpbnd1  25320  pntlem3  25343  padicabvf  25365  axcontlem2  25890  nbgrnself  26300  vtxdginducedm1  26495  isgrpoi  27480  isvciOLD  27563  cnidOLD  27565  isnvi  27596  ipasslem8  27820  hilid  28146  hlimf  28222  shsspwh  28231  pjrni  28689  pjmf1  28703  df0op2  28739  dfiop2  28740  hoaddcomi  28759  hoaddassi  28763  hocadddiri  28766  hocsubdiri  28767  hoaddid1i  28773  ho0coi  28775  hoid1i  28776  hoid1ri  28777  honegsubi  28783  hoddii  28976  lnopunilem2  28998  elunop2  29000  lnophm  29006  imaelshi  29045  cnlnadjlem8  29061  pjnmopi  29135  pjsdii  29142  pjddii  29143  pjtoi  29166  chirred  29382  nnindf  29693  nn0min  29695  esum2d  30283  dmvlsiga  30320  volmeas  30422  ddemeas  30427  sxbrsigalem3  30462  coinfliprv  30672  ballotlem7  30725  signsw0glem  30758  rpsqrtcn  30799  tgoldbachgt  30869  bnj580  31109  bnj1384  31226  bnj1497  31254  kur14lem9  31322  msrf  31565  dfon2lem7  31818  frinsg  31870  bdayfo  31953  nodense  31967  fobigcup  32132  nn0prpwlem  32442  topmeet  32484  onsucsuccmpi  32567  taupilemrplb  33296  relowlssretop  33341  ptrecube  33539  poimirlem27  33566  heicant  33574  mblfinlem1  33576  volsupnfl  33584  dvtan  33590  itg2addnc  33594  indexa  33658  sstotbnd2  33703  heiborlem7  33746  atpsubN  35357  idldil  35718  cdleme50ldil  36153  mzpclall  37607  dgraaf  38034  arearect  38118  areaquad  38119  clsk1indlem2  38657  clsk1indlem4  38659  prmunb2  38827  radcnvrat  38830  unirnmapsn  39720  ssmapsn  39722  upbdrech  39833  supminfxr  40007  supminfxr2  40012  supminfxrrnmpt  40014  fsumiunss  40125  resincncf  40406  dmvolss  40520  volioof  40522  stoweidlem57  40592  wallispilem3  40602  stirlinglem13  40621  dirkertrigeqlem3  40635  fourierdlem62  40703  salexct  40870  salexct3  40878  salgencntex  40879  salgensscntex  40880  gsumge0cl  40906  0ome  41064  icoresmbl  41078  hoidmv1le  41129  smflimlem1  41300  smfpimbor1lem2  41327  smfliminflem  41357  fmtno4prm  41812  31prm  41837  tgoldbach  42030  tgoldbachOLD  42037  2zlidl  42259  2zrngagrp  42268  2zrngnmlid  42274  crhmsubc  42403  drhmsubc  42405  drngcat  42406  fldcat  42407  fldhmsubc  42409  crhmsubcALTV  42421  drhmsubcALTV  42423  drngcatALTV  42424  fldcatALTV  42425  fldhmsubcALTV  42427  zlmodzxznm  42611  ldepsnlinc  42622  nn0sumshdiglem2  42741  onsetrec  42779
  Copyright terms: Public domain W3C validator