Theorem rgenw 3051

Description: Generalization rule for restricted quantification. (Contributed by NM, 18-Jun-2014.)

Hypothesis

Ref	Expression
rgenw.1	⊢ 𝜑

Assertion

Ref	Expression
rgenw	⊢ ∀𝑥 ∈ 𝐴 𝜑

Proof of Theorem rgenw

Step	Hyp	Ref	Expression
1		rgenw.1	. . 3 ⊢ 𝜑
2	1	a1i 11	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝜑)
3	2	rgen 3049	1 ⊢ ∀𝑥 ∈ 𝐴 𝜑

Syntax hints:   ∈ wcel 2111  ∀wral 3047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796

This theorem depends on definitions:  df-bi 207  df-ral 3048

This theorem is referenced by:  rgen2w  3052  reuss  4274  reuun1  4275  rabnc  4338  riinrab  5030  0disj  5082  iinexg  5284  epse  5596  xpiindi  5774  eliunxp  5776  opeliunxp2  5777  elrnmpti  5901  cnviin  6233  fnmpti  6624  eqfnfv  6964  eufnfv  7163  mpoeq12  7419  porpss  7660  iunex  7900  abrexex2  7901  mpoex  8011  suppssov1  8127  suppssov2  8128  suppssfv  8132  opeliunxp2f  8140  onnseq  8264  ixpssmap  8856  boxcutc  8865  nneneq  9115  finsschain  9243  dfom3  9537  cantnfdm  9554  rankuni2b  9746  rankval4  9760  alephf1  9976  dfac4  10013  dfacacn  10033  infmap2  10108  cfeq0  10147  fin23lem28  10231  axdc2lem  10339  axcclem  10348  ac6  10371  iundom  10433  konigthlem  10459  iunctb  10465  tskmid  10731  supaddc  12089  supadd  12090  supmul1  12091  supmullem2  12093  supmul  12094  uzf  12735  seqof  13966  hashbclem  14359  rlimclim1  15452  fsumcom2  15681  ackbijnn  15735  fprodcom2  15891  lcmf0  16545  phisum  16702  sumhash  16808  ramcl  16941  prdsvallem  17358  prdsval  17359  prdsbas  17361  prdshom  17371  imasplusg  17421  imasmulr  17422  imasvsca  17424  imasip  17425  imasaddfnlem  17432  imasvscafn  17441  isfunc  17771  wunfunc  17808  isnat  17857  natffn  17859  wunnat  17866  fucsect  17882  setcepi  17995  grpinvfval  18891  odfval  19444  dfod2  19476  ghmcyg  19808  gsum2d2lem  19885  gsum2d2  19886  gsumcom2  19887  dmdprd  19912  dprdval  19917  dprdf11  19937  dprd2d2  19958  dpjeq  19973  pgpfac1lem2  19989  pgpfac1lem3  19991  pgpfac1lem4  19992  mptscmfsupp0  20860  00lsp  20914  ocv0  21614  ofco2  22366  tgidm  22895  pptbas  22923  tgrest  23074  iscnp2  23154  ist1-3  23264  discmp  23313  1stcfb  23360  lly1stc  23411  disllycmp  23413  dis1stc  23414  comppfsc  23447  txbas  23482  ptbasfi  23496  ptpjopn  23527  dfac14  23533  ptrescn  23554  xkoptsub  23569  fclsval  23923  ptcmplem2  23968  ptcmplem3  23969  cnextrel  23978  tsmsfbas  24043  ustuqtop  24161  prdsxmetlem  24283  ressprdsds  24286  prdsxmslem2  24444  zcld  24729  xrge0tsms  24750  metdsf  24764  metdsge  24765  minveclem1  25351  minveclem3b  25355  minveclem6  25361  uniioombllem4  25514  uniioombllem6  25516  ismbf3d  25582  i1f1lem  25617  reldv  25798  ellimc2  25805  limcflf  25809  limciun  25822  dvfval  25825  dvrec  25886  dvlipcn  25926  mdegle0  26009  ply1nzb  26055  quotlem  26235  taylfval  26293  ulmdvlem1  26336  ulmdvlem2  26337  ulmdvlem3  26338  psercn  26363  sqff1o  27119  lgsquadlem2  27319  bdayiun  27860  disjxwwlksn  29882  disjxwwlkn  29891  numclwwlk3lem2  30364  grpoidval  30493  grpoidinv2  30495  grpoinv  30505  minvecolem1  30854  minvecolem5  30861  minvecolem6  30862  adjbdln  32063  dfcnv2  32658  intimafv  32692  rexdiv  32906  gsumpart  33037  xrge0tsmsd  33042  fedgmullem2  33643  irngval  33698  rspectopn  33880  zarcls  33887  zartopn  33888  esumnul  34061  esum0  34062  hasheuni  34098  esum2d  34106  ldgenpisyslem3  34178  measvuni  34227  measdivcstALTV  34238  ddemeas  34249  carsgclctunlem2  34332  eulerpartlemgs2  34393  probfinmeasbALTV  34442  0rrv  34464  signsplypnf  34563  signsply0  34564  hgt750lemb  34669  bnj226  34746  bnj98  34879  bnj517  34897  bnj893  34940  bnj1137  35007  rankval4b  35111  rankfilimbi  35112  tz9.1regs  35130  fineqvnttrclse  35144  subfacf  35219  subfacp1lem6  35229  cvmsss2  35318  cvmliftlem1  35329  ixpeq12i  36245  bj-rabtr  36974  relowlssretop  37407  fin2so  37657  matunitlindflem1  37666  ptrest  37669  poimirlem23  37693  poimirlem24  37694  poimirlem27  37697  poimirlem30  37700  poimirlem32  37702  cnambfre  37718  upixp  37779  0totbnd  37823  prdsbnd  37843  prdstotbnd  37844  cntotbnd  37846  rrnequiv  37885  ac6s6  38222  dmsucmap  38491  cdlemefrs32fva  40509  cdlemkid5  41044  cdlemk56  41080  dihf11lem  41375  addinvcom  42535  0dioph  42881  vdioph  42882  pw2f1ocnv  43140  pwinfi  43667  eliunov2  43782  fvmptiunrelexplb0d  43787  fvmptiunrelexplb1d  43789  iunrelexp0  43805  ntrrn  44225  dssmapntrcls  44231  mnurndlem1  44384  rankrelp  45063  0elaxnul  45086  prclaxpr  45088  uniclaxun  45089  omssaxinf2  45091  wessf1ornlem  45292  axccdom  45329  fnmptif  45372  fsumiunss  45685  limcdm0  45728  liminfval2  45876  liminflelimsuplem  45883  cnrefiisplem  45937  0cnf  45985  dvsinax  46021  ioodvbdlimc1lem2  46040  ioodvbdlimc2lem  46042  dvnprodlem3  46056  iblempty  46073  fourierdlem89  46303  fourierdlem91  46305  fourierdlem100  46314  fourierdlem108  46322  fourierdlem112  46326  salexct3  46450  salgensscntex  46452  omeiunle  46625  0ome  46637  hoissrrn  46657  ovn0  46674  hoissrrn2  46686  hspmbl  46737  ovolval5lem2  46761  iunhoiioolem  46783  vonioolem2  46789  vonicclem2  46792  smflimlem1  46879  smfsuplem1  46919  smfinflem  46925  smflimsuplem1  46928  smflimsuplem2  46929  smflimsuplem3  46930  smflimsuplem4  46931  smflimsuplem5  46932  smflimsuplem7  46934  smfliminflem  46938  nthrucw  46994  ralndv2  47216  iccelpart  47543  eliunxp2  48444  1arymaptf1  48753  iinxp  48941  iinfssclem2  49166  iinfssclem3  49167  iinfssc  49168  imasubclem1  49215