Theorem rgenw 3066

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 3064	1 ⊢ ∀𝑥 ∈ 𝐴 𝜑

Syntax hints:   ∈ wcel 2106  ∀wral 3062

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

This theorem depends on definitions:  df-bi 206  df-ral 3063

This theorem is referenced by:  rgen2w  3067  reuss  4268  reuun1  4269  rabnc  4339  riinrab  5036  0disj  5089  iinexg  5290  epse  5608  xpiindi  5782  eliunxp  5784  opeliunxp2  5785  elrnmpti  5906  cnviin  6229  fnmpti  6632  eqfnfv  6970  eufnfv  7166  mpoeq12  7415  porpss  7647  iunex  7884  abrexex2  7885  mpoex  7993  suppssov1  8089  suppssfv  8093  opeliunxp2f  8101  onnseq  8250  ixpssmap  8796  boxcutc  8805  nneneq  9079  nneneqOLD  9091  finsschain  9229  dfom3  9509  cantnfdm  9526  rankuni2b  9715  rankval4  9729  alephf1  9947  dfac4  9984  dfacacn  10003  infmap2  10080  cfeq0  10118  fin23lem28  10202  axdc2lem  10310  axcclem  10319  ac6  10342  iundom  10404  konigthlem  10430  iunctb  10436  tskmid  10702  supaddc  12048  supadd  12049  supmul1  12050  supmullem2  12052  supmul  12053  uzf  12691  seqof  13886  hashbclem  14269  rlimclim1  15354  fsumcom2  15586  ackbijnn  15640  fprodcom2  15794  lcmf0  16437  phisum  16589  sumhash  16695  ramcl  16828  prdsvallem  17263  prdsval  17264  prdsbas  17266  prdshom  17276  imasplusg  17326  imasmulr  17327  imasvsca  17329  imasip  17330  imasaddfnlem  17337  imasvscafn  17346  isfunc  17677  wunfunc  17712  wunfuncOLD  17713  isnat  17761  natffn  17763  wunnat  17770  wunnatOLD  17771  fucsect  17788  setcepi  17901  grpinvfval  18715  odfval  19237  dfod2  19268  ghmcyg  19592  gsum2d2lem  19669  gsum2d2  19670  gsumcom2  19671  dmdprd  19696  dprdval  19701  dprdf11  19721  dprd2d2  19742  dpjeq  19757  pgpfac1lem2  19773  pgpfac1lem3  19775  pgpfac1lem4  19776  mptscmfsupp0  20294  00lsp  20349  ocv0  20988  ofco2  21706  tgidm  22236  pptbas  22264  tgrest  22416  iscnp2  22496  ist1-3  22606  discmp  22655  1stcfb  22702  lly1stc  22753  disllycmp  22755  dis1stc  22756  comppfsc  22789  txbas  22824  ptbasfi  22838  ptpjopn  22869  dfac14  22875  ptrescn  22896  xkoptsub  22911  fclsval  23265  ptcmplem2  23310  ptcmplem3  23311  cnextrel  23320  tsmsfbas  23385  ustuqtop  23504  prdsxmetlem  23627  ressprdsds  23630  prdsxmslem2  23791  zcld  24082  xrge0tsms  24103  metdsf  24117  metdsge  24118  minveclem1  24694  minveclem3b  24698  minveclem6  24704  uniioombllem4  24856  uniioombllem6  24858  ismbf3d  24924  i1f1lem  24959  reldv  25140  ellimc2  25147  limcflf  25151  limciun  25164  dvfval  25167  dvrec  25225  dvlipcn  25264  mdegle0  25348  ply1nzb  25393  quotlem  25566  taylfval  25624  ulmdvlem1  25665  ulmdvlem2  25666  ulmdvlem3  25667  psercn  25691  sqff1o  26437  lgsquadlem2  26635  disjxwwlksn  28557  disjxwwlkn  28566  numclwwlk3lem2  29036  grpoidval  29163  grpoidinv2  29165  grpoinv  29175  minvecolem1  29524  minvecolem5  29531  minvecolem6  29532  adjbdln  30733  dfcnv2  31298  intimafv  31328  rexdiv  31485  gsumpart  31600  xrge0tsmsd  31602  fedgmullem2  32007  rspectopn  32113  zarcls  32120  zartopn  32121  esumnul  32312  esum0  32313  hasheuni  32349  esum2d  32357  ldgenpisyslem3  32429  measvuni  32478  measdivcstALTV  32489  ddemeas  32500  carsgclctunlem2  32584  eulerpartlemgs2  32645  probfinmeasbALTV  32694  0rrv  32716  signsplypnf  32827  signsply0  32828  hgt750lemb  32934  bnj226  33011  bnj98  33144  bnj517  33162  bnj893  33205  bnj1137  33272  subfacf  33434  subfacp1lem6  33444  cvmsss2  33533  cvmliftlem1  33544  bj-rabtr  35254  relowlssretop  35688  fin2so  35918  matunitlindflem1  35927  ptrest  35930  poimirlem23  35954  poimirlem24  35955  poimirlem27  35958  poimirlem30  35961  poimirlem32  35963  cnambfre  35979  upixp  36041  0totbnd  36085  prdsbnd  36105  prdstotbnd  36106  cntotbnd  36108  rrnequiv  36147  ac6s6  36484  cdlemefrs32fva  38717  cdlemkid5  39252  cdlemk56  39288  dihf11lem  39583  addinvcom  40722  0dioph  40911  vdioph  40912  rmxyelqirrOLD  41044  pw2f1ocnv  41171  pwinfi  41543  eliunov2  41658  fvmptiunrelexplb0d  41663  fvmptiunrelexplb1d  41665  iunrelexp0  41681  ntrrn  42103  dssmapntrcls  42109  mnurndlem1  42270  wessf1ornlem  43099  axccdom  43139  mpteq1dfOLD  43158  fnmptif  43191  fsumiunss  43502  limcdm0  43545  liminfval2  43695  liminflelimsuplem  43702  cnrefiisplem  43756  0cnf  43804  dvsinax  43840  ioodvbdlimc1lem2  43859  ioodvbdlimc2lem  43861  dvnprodlem3  43875  iblempty  43892  fourierdlem89  44122  fourierdlem91  44124  fourierdlem100  44133  fourierdlem108  44141  fourierdlem112  44145  salexct3  44267  salgensscntex  44269  omeiunle  44442  0ome  44454  hoissrrn  44474  ovn0  44491  hoissrrn2  44503  hspmbl  44554  ovolval5lem2  44578  iunhoiioolem  44600  vonioolem2  44606  vonicclem2  44609  smflimlem1  44696  smfsuplem1  44736  smfinflem  44742  smflimsuplem1  44745  smflimsuplem2  44746  smflimsuplem3  44747  smflimsuplem4  44748  smflimsuplem5  44749  smflimsuplem7  44751  smfliminflem  44755  ralndv2  45014  iccelpart  45301  eliunxp2  46085  1arymaptf1  46404