Theorem rgenw 3080

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

Syntax hints:   ∈ wcel 2142  ∀wral 3076

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

This theorem depends on definitions:  df-bi 209  df-ral 3077

This theorem is referenced by:  rgen2w  3081  reuss  4279  reuun1  4280  rabnc  4345  riinrab  5041  0disj  5093  iinexg  5304  epse  5629  xpiindi  5807  eliunxp  5809  opeliunxp2  5810  elrnmpti  5938  cnviin  6273  fnmpti  6664  eqfnfv  7011  eufnfv  7213  mpoeq12  7469  porpss  7710  iunex  7949  abrexex2  7950  mpoex  8060  suppssov1  8177  suppssov2  8178  suppssfv  8182  opeliunxp2f  8190  onnseq  8315  ixpssmap  8914  boxcutc  8923  nneneq  9174  finsschain  9302  dfom3  9602  cantnfdm  9619  rankuni2b  9811  rankval4  9825  alephf1  10041  dfac4  10078  dfacacn  10098  infmap2  10173  cfeq0  10213  fin23lem28  10297  axdc2lem  10405  axcclem  10414  ac6  10437  iundom  10499  konigthlem  10526  iunctb  10532  tskmid  10798  supaddc  12159  supadd  12160  supmul1  12161  supmullem2  12163  supmul  12164  uzf  12842  seqof  14072  hashbclem  14465  rlimclim1  15572  fsumcom2  15801  ackbijnn  15858  fprodcom2  16014  lcmf0  16668  phisum  16826  sumhash  16932  ramcl  17065  prdsvallem  17483  prdsval  17484  prdsbas  17486  prdshom  17496  imasplusg  17547  imasmulr  17548  imasvsca  17550  imasip  17551  imasaddfnlem  17558  imasvscafn  17567  isfunc  17897  wunfunc  17934  isnat  17983  natffn  17985  wunnat  17992  fucsect  18008  setcepi  18121  grpinvfval  19020  odfval  19572  dfod2  19604  ghmcyg  19936  gsum2d2lem  20013  gsum2d2  20014  gsumcom2  20015  dmdprd  20040  dprdval  20045  dprdf11  20065  dprd2d2  20086  dpjeq  20101  pgpfac1lem2  20117  pgpfac1lem3  20119  pgpfac1lem4  20120  mptscmfsupp0  20994  00lsp  21048  ocv0  21729  ofco2  22511  tgidm  23040  pptbas  23068  tgrest  23219  iscnp2  23299  ist1-3  23409  discmp  23458  1stcfb  23505  lly1stc  23556  disllycmp  23558  dis1stc  23559  comppfsc  23592  txbas  23627  ptbasfi  23641  ptpjopn  23672  dfac14  23678  ptrescn  23699  xkoptsub  23714  fclsval  24068  ptcmplem2  24113  ptcmplem3  24114  cnextrel  24123  tsmsfbas  24188  ustuqtop  24306  prdsxmetlem  24428  ressprdsds  24431  prdsxmslem2  24589  zcld  24874  xrge0tsms  24895  metdsf  24909  metdsge  24910  minveclem1  25486  minveclem3b  25490  minveclem6  25496  uniioombllem4  25648  uniioombllem6  25650  ismbf3d  25716  i1f1lem  25751  reldv  25932  ellimc2  25939  limcflf  25943  limciun  25956  dvfval  25959  dvrec  26017  dvlipcn  26056  mdegle0  26137  ply1nzb  26183  quotlem  26364  taylfval  26422  ulmdvlem1  26463  ulmdvlem2  26464  ulmdvlem3  26465  psercn  26489  sqff1o  27246  lgsquadlem2  27445  bdayiun  28008  disjxwwlksn  30104  disjxwwlkn  30113  numclwwlk3lem2  30586  grpoidval  30716  grpoidinv2  30718  grpoinv  30728  minvecolem1  31077  minvecolem5  31084  minvecolem6  31085  adjbdln  32286  dfcnv2  32877  intimafv  32913  rexdiv  33103  gsumpart  33243  xrge0tsmsd  33253  fedgmullem2  33927  irngval  33982  rspectopn  34164  zarcls  34171  zartopn  34172  esumnul  34345  esum0  34346  hasheuni  34382  esum2d  34390  ldgenpisyslem3  34462  measvuni  34511  measdivcstALTV  34522  ddemeas  34533  carsgclctunlem2  34616  eulerpartlemgs2  34677  probfinmeasbALTV  34726  0rrv  34748  signsplypnf  34844  signsply0  34845  hgt750lemb  34950  bnj226  35030  bnj98  35162  bnj517  35180  bnj893  35223  bnj1137  35290  rankval4b  35396  rankfilimbi  35397  fineqvnttrclse  35420  tz9.1regs  35430  subfacf  35525  subfacp1lem6  35535  cvmsss2  35624  cvmliftlem1  35635  nmulr0  36545  ixpeq12i  36561  ttciunun  36871  bj-rabtr  37415  bj-axseprep  37559  relowlssretop  37857  fin2so  38106  matunitlindflem1  38115  ptrest  38118  poimirlem23  38142  poimirlem24  38143  poimirlem27  38146  poimirlem30  38149  poimirlem32  38151  cnambfre  38167  upixp  38228  0totbnd  38272  prdsbnd  38292  prdstotbnd  38293  cntotbnd  38295  rrnequiv  38334  ac6s6  38671  dmsucmap  38967  disjimeceqim  39303  cdlemefrs32fva  41024  cdlemkid5  41559  cdlemk56  41595  dihf11lem  41890  addinvcom  43041  0dioph  43359  vdioph  43360  pw2f1ocnv  43614  pwinfi  44140  eliunov2  44255  fvmptiunrelexplb0d  44260  fvmptiunrelexplb1d  44262  iunrelexp0  44278  ntrrn  44698  dssmapntrcls  44704  mnurndlem1  44857  rankrelp  45536  0elaxnul  45559  prclaxpr  45561  uniclaxun  45562  omssaxinf2  45564  wessf1ornlem  45763  axccdom  45798  fnmptif  45840  fsumiunss  46151  limcdm0  46194  liminfval2  46342  liminflelimsuplem  46349  cnrefiisplem  46403  0cnf  46451  dvsinax  46487  ioodvbdlimc1lem2  46506  ioodvbdlimc2lem  46508  dvnprodlem3  46522  iblempty  46539  fourierdlem89  46769  fourierdlem91  46771  fourierdlem100  46780  fourierdlem108  46788  fourierdlem112  46792  salexct3  46916  salgensscntex  46918  omeiunle  47091  0ome  47103  hoissrrn  47123  ovn0  47140  hoissrrn2  47152  hspmbl  47203  ovolval5lem2  47227  iunhoiioolem  47249  vonioolem2  47255  vonicclem2  47258  smflimlem1  47345  smfsuplem1  47385  smfinflem  47391  smflimsuplem1  47394  smflimsuplem2  47395  smflimsuplem3  47396  smflimsuplem4  47397  smflimsuplem5  47398  smflimsuplem7  47400  smfliminflem  47404  nthrucw  47462  ralndv2  47700  iccelpart  48039  eliunxp2  48956  1arymaptf1  49264  iinxp  49452  iinfssclem2  49676  iinfssclem3  49677  iinfssc  49678  imasubclem1  49725