Theorem rgenw 3048

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

Syntax hints:   ∈ wcel 2109  ∀wral 3044

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

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

This theorem is referenced by:  rgen2w  3049  reuss  4290  reuun1  4291  rabnc  4354  riinrab  5048  0disj  5100  iinexg  5303  epse  5620  xpiindi  5799  eliunxp  5801  opeliunxp2  5802  elrnmpti  5926  cnviin  6259  fnmpti  6661  eqfnfv  7003  eufnfv  7203  mpoeq12  7462  porpss  7703  iunex  7947  abrexex2  7948  mpoex  8058  suppssov1  8176  suppssov2  8177  suppssfv  8181  opeliunxp2f  8189  onnseq  8313  ixpssmap  8905  boxcutc  8914  nneneq  9170  finsschain  9310  dfom3  9600  cantnfdm  9617  rankuni2b  9806  rankval4  9820  alephf1  10038  dfac4  10075  dfacacn  10095  infmap2  10170  cfeq0  10209  fin23lem28  10293  axdc2lem  10401  axcclem  10410  ac6  10433  iundom  10495  konigthlem  10521  iunctb  10527  tskmid  10793  supaddc  12150  supadd  12151  supmul1  12152  supmullem2  12154  supmul  12155  uzf  12796  seqof  14024  hashbclem  14417  rlimclim1  15511  fsumcom2  15740  ackbijnn  15794  fprodcom2  15950  lcmf0  16604  phisum  16761  sumhash  16867  ramcl  17000  prdsvallem  17417  prdsval  17418  prdsbas  17420  prdshom  17430  imasplusg  17480  imasmulr  17481  imasvsca  17483  imasip  17484  imasaddfnlem  17491  imasvscafn  17500  isfunc  17826  wunfunc  17863  isnat  17912  natffn  17914  wunnat  17921  fucsect  17937  setcepi  18050  grpinvfval  18910  odfval  19462  dfod2  19494  ghmcyg  19826  gsum2d2lem  19903  gsum2d2  19904  gsumcom2  19905  dmdprd  19930  dprdval  19935  dprdf11  19955  dprd2d2  19976  dpjeq  19991  pgpfac1lem2  20007  pgpfac1lem3  20009  pgpfac1lem4  20010  mptscmfsupp0  20833  00lsp  20887  ocv0  21586  ofco2  22338  tgidm  22867  pptbas  22895  tgrest  23046  iscnp2  23126  ist1-3  23236  discmp  23285  1stcfb  23332  lly1stc  23383  disllycmp  23385  dis1stc  23386  comppfsc  23419  txbas  23454  ptbasfi  23468  ptpjopn  23499  dfac14  23505  ptrescn  23526  xkoptsub  23541  fclsval  23895  ptcmplem2  23940  ptcmplem3  23941  cnextrel  23950  tsmsfbas  24015  ustuqtop  24134  prdsxmetlem  24256  ressprdsds  24259  prdsxmslem2  24417  zcld  24702  xrge0tsms  24723  metdsf  24737  metdsge  24738  minveclem1  25324  minveclem3b  25328  minveclem6  25334  uniioombllem4  25487  uniioombllem6  25489  ismbf3d  25555  i1f1lem  25590  reldv  25771  ellimc2  25778  limcflf  25782  limciun  25795  dvfval  25798  dvrec  25859  dvlipcn  25899  mdegle0  25982  ply1nzb  26028  quotlem  26208  taylfval  26266  ulmdvlem1  26309  ulmdvlem2  26310  ulmdvlem3  26311  psercn  26336  sqff1o  27092  lgsquadlem2  27292  disjxwwlksn  29834  disjxwwlkn  29843  numclwwlk3lem2  30313  grpoidval  30442  grpoidinv2  30444  grpoinv  30454  minvecolem1  30803  minvecolem5  30810  minvecolem6  30811  adjbdln  32012  dfcnv2  32600  intimafv  32634  rexdiv  32846  gsumpart  32997  xrge0tsmsd  33002  fedgmullem2  33626  irngval  33680  rspectopn  33857  zarcls  33864  zartopn  33865  esumnul  34038  esum0  34039  hasheuni  34075  esum2d  34083  ldgenpisyslem3  34155  measvuni  34204  measdivcstALTV  34215  ddemeas  34226  carsgclctunlem2  34310  eulerpartlemgs2  34371  probfinmeasbALTV  34420  0rrv  34442  signsplypnf  34541  signsply0  34542  hgt750lemb  34647  bnj226  34724  bnj98  34857  bnj517  34875  bnj893  34918  bnj1137  34985  subfacf  35162  subfacp1lem6  35172  cvmsss2  35261  cvmliftlem1  35272  ixpeq12i  36189  bj-rabtr  36918  relowlssretop  37351  fin2so  37601  matunitlindflem1  37610  ptrest  37613  poimirlem23  37637  poimirlem24  37638  poimirlem27  37641  poimirlem30  37644  poimirlem32  37646  cnambfre  37662  upixp  37723  0totbnd  37767  prdsbnd  37787  prdstotbnd  37788  cntotbnd  37790  rrnequiv  37829  ac6s6  38166  cdlemefrs32fva  40394  cdlemkid5  40929  cdlemk56  40965  dihf11lem  41260  addinvcom  42420  0dioph  42766  vdioph  42767  rmxyelqirrOLD  42899  pw2f1ocnv  43026  pwinfi  43553  eliunov2  43668  fvmptiunrelexplb0d  43673  fvmptiunrelexplb1d  43675  iunrelexp0  43691  ntrrn  44111  dssmapntrcls  44117  mnurndlem1  44270  rankrelp  44950  0elaxnul  44973  prclaxpr  44975  uniclaxun  44976  omssaxinf2  44978  wessf1ornlem  45179  axccdom  45216  fnmptif  45259  fsumiunss  45573  limcdm0  45616  liminfval2  45766  liminflelimsuplem  45773  cnrefiisplem  45827  0cnf  45875  dvsinax  45911  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvnprodlem3  45946  iblempty  45963  fourierdlem89  46193  fourierdlem91  46195  fourierdlem100  46204  fourierdlem108  46212  fourierdlem112  46216  salexct3  46340  salgensscntex  46342  omeiunle  46515  0ome  46527  hoissrrn  46547  ovn0  46564  hoissrrn2  46576  hspmbl  46627  ovolval5lem2  46651  iunhoiioolem  46673  vonioolem2  46679  vonicclem2  46682  smflimlem1  46769  smfsuplem1  46809  smfinflem  46815  smflimsuplem1  46818  smflimsuplem2  46819  smflimsuplem3  46820  smflimsuplem4  46821  smflimsuplem5  46822  smflimsuplem7  46824  smfliminflem  46828  ralndv2  47107  iccelpart  47434  eliunxp2  48322  1arymaptf1  48631  iinxp  48819  iinfssclem2  49044  iinfssclem3  49045  iinfssc  49046  imasubclem1  49093