Theorem rgenw 3063

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

Syntax hints:   ∈ wcel 2112  ∀wral 3051

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

This theorem depends on definitions:  df-bi 210  df-ral 3056

This theorem is referenced by:  rgen2w  3064  reuss  4217  reuun1  4218  rabnc  4288  riinrab  4978  0disj  5031  iinexg  5219  epse  5519  xpiindi  5689  eliunxp  5691  opeliunxp2  5692  elrnmpti  5814  cnviin  6129  fnmpti  6499  eqfnfv  6830  mptexgf  7016  eufnfv  7023  mpoeq12  7262  porpss  7493  iunex  7719  abrexex2  7720  mpoex  7828  suppssov1  7918  suppssfv  7922  opeliunxp2f  7930  onnseq  8059  ixpssmap  8591  boxcutc  8600  nneneq  8807  finsschain  8961  dfom3  9240  cantnfdm  9257  rankuni2b  9434  rankval4  9448  alephf1  9664  dfac4  9701  dfacacn  9720  infmap2  9797  cfeq0  9835  fin23lem28  9919  axdc2lem  10027  axcclem  10036  ac6  10059  iundom  10121  konigthlem  10147  iunctb  10153  tskmid  10419  supaddc  11764  supadd  11765  supmul1  11766  supmullem2  11768  supmul  11769  uzf  12406  seqof  13598  hashbclem  13981  rlimclim1  15071  fsumcom2  15301  ackbijnn  15355  fprodcom2  15509  lcmf0  16154  phisum  16306  sumhash  16412  ramcl  16545  prdsvallem  16913  prdsval  16914  prdsbas  16916  prdshom  16926  imasplusg  16976  imasmulr  16977  imasvsca  16979  imasip  16980  imasaddfnlem  16987  imasvscafn  16996  isfunc  17324  wunfunc  17359  wunfuncOLD  17360  isnat  17408  natffn  17410  wunnat  17417  wunnatOLD  17418  fucsect  17435  setcepi  17548  grpinvfval  18360  odfval  18878  dfod2  18909  ghmcyg  19235  gsum2d2lem  19312  gsum2d2  19313  gsumcom2  19314  dmdprd  19339  dprdval  19344  dprdf11  19364  dprd2d2  19385  dpjeq  19400  pgpfac1lem2  19416  pgpfac1lem3  19418  pgpfac1lem4  19419  mptscmfsupp0  19918  00lsp  19972  ocv0  20593  ofco2  21302  tgidm  21831  pptbas  21859  tgrest  22010  iscnp2  22090  ist1-3  22200  discmp  22249  1stcfb  22296  lly1stc  22347  disllycmp  22349  dis1stc  22350  comppfsc  22383  txbas  22418  ptbasfi  22432  ptpjopn  22463  dfac14  22469  ptrescn  22490  xkoptsub  22505  fclsval  22859  ptcmplem2  22904  ptcmplem3  22905  cnextrel  22914  tsmsfbas  22979  ustuqtop  23098  prdsxmetlem  23220  ressprdsds  23223  prdsxmslem2  23381  zcld  23664  xrge0tsms  23685  metdsf  23699  metdsge  23700  minveclem1  24275  minveclem3b  24279  minveclem6  24285  uniioombllem4  24437  uniioombllem6  24439  ismbf3d  24505  i1f1lem  24540  reldv  24721  ellimc2  24728  limcflf  24732  limciun  24745  dvfval  24748  dvrec  24806  dvlipcn  24845  mdegle0  24929  ply1nzb  24974  quotlem  25147  taylfval  25205  ulmdvlem1  25246  ulmdvlem2  25247  ulmdvlem3  25248  psercn  25272  sqff1o  26018  lgsquadlem2  26216  disjxwwlksn  27942  wwlksnfi  27944  disjxwwlkn  27951  numclwwlk3lem2  28421  grpoidval  28548  grpoidinv2  28550  grpoinv  28560  minvecolem1  28909  minvecolem5  28916  minvecolem6  28917  adjbdln  30118  dfcnv2  30687  intimafv  30717  rexdiv  30874  gsumpart  30988  xrge0tsmsd  30990  fedgmullem2  31379  rspectopn  31485  zarcls  31492  zartopn  31493  esumnul  31682  esum0  31683  hasheuni  31719  esum2d  31727  ldgenpisyslem3  31799  measvuni  31848  measdivcstALTV  31859  ddemeas  31870  carsgclctunlem2  31952  eulerpartlemgs2  32013  probfinmeasbALTV  32062  0rrv  32084  signsplypnf  32195  signsply0  32196  hgt750lemb  32302  bnj226  32379  bnj98  32514  bnj517  32532  bnj893  32575  bnj1137  32642  subfacf  32804  subfacp1lem6  32814  cvmsss2  32903  cvmliftlem1  32914  bj-rabtr  34804  relowlssretop  35220  fin2so  35450  matunitlindflem1  35459  ptrest  35462  poimirlem23  35486  poimirlem24  35487  poimirlem27  35490  poimirlem30  35493  poimirlem32  35495  cnambfre  35511  upixp  35573  0totbnd  35617  prdsbnd  35637  prdstotbnd  35638  cntotbnd  35640  rrnequiv  35679  ac6s6  36016  cdlemefrs32fva  38100  cdlemkid5  38635  cdlemk56  38671  dihf11lem  38966  addinvcom  40062  0dioph  40244  vdioph  40245  rmxyelqirr  40376  pw2f1ocnv  40503  pwinfi  40788  eliunov2  40905  fvmptiunrelexplb0d  40910  fvmptiunrelexplb1d  40912  iunrelexp0  40928  ntrrn  41350  dssmapntrcls  41356  mnurndlem1  41513  wessf1ornlem  42336  axccdom  42376  mpteq1df  42393  fsumiunss  42734  limcdm0  42777  liminfval2  42927  liminflelimsuplem  42934  cnrefiisplem  42988  0cnf  43036  dvsinax  43072  ioodvbdlimc1lem2  43091  ioodvbdlimc2lem  43093  dvnprodlem3  43107  iblempty  43124  fourierdlem89  43354  fourierdlem91  43356  fourierdlem100  43365  fourierdlem108  43373  fourierdlem112  43377  salexct3  43499  salgensscntex  43501  omeiunle  43673  0ome  43685  hoissrrn  43705  ovn0  43722  hoissrrn2  43734  hspmbl  43785  ovolval5lem2  43809  ovolval5lem3  43810  iunhoiioolem  43831  vonioolem2  43837  vonicclem2  43840  smflimlem1  43921  smfsuplem1  43959  smfinflem  43965  smflimsuplem1  43968  smflimsuplem2  43969  smflimsuplem3  43970  smflimsuplem4  43971  smflimsuplem5  43972  smflimsuplem7  43974  smfliminflem  43978  ralndv2  44213  iccelpart  44501  eliunxp2  45285  1arymaptf1  45604