Theorem rgenw 3056

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

Syntax hints:   ∈ wcel 2114  ∀wral 3052

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 207  df-ral 3053

This theorem is referenced by:  rgen2w  3057  reuss  4268  reuun1  4269  rabnc  4332  riinrab  5027  0disj  5079  iinexg  5286  epse  5607  xpiindi  5785  eliunxp  5787  opeliunxp2  5788  elrnmpti  5912  cnviin  6245  fnmpti  6636  eqfnfv  6978  eufnfv  7178  mpoeq12  7434  porpss  7675  iunex  7915  abrexex2  7916  mpoex  8026  suppssov1  8141  suppssov2  8142  suppssfv  8146  opeliunxp2f  8154  onnseq  8278  ixpssmap  8874  boxcutc  8883  nneneq  9134  finsschain  9263  dfom3  9562  cantnfdm  9579  rankuni2b  9771  rankval4  9785  alephf1  10001  dfac4  10038  dfacacn  10058  infmap2  10133  cfeq0  10172  fin23lem28  10256  axdc2lem  10364  axcclem  10373  ac6  10396  iundom  10458  konigthlem  10485  iunctb  10491  tskmid  10757  supaddc  12117  supadd  12118  supmul1  12119  supmullem2  12121  supmul  12122  uzf  12785  seqof  14015  hashbclem  14408  rlimclim1  15501  fsumcom2  15730  ackbijnn  15787  fprodcom2  15943  lcmf0  16597  phisum  16755  sumhash  16861  ramcl  16994  prdsvallem  17411  prdsval  17412  prdsbas  17414  prdshom  17424  imasplusg  17475  imasmulr  17476  imasvsca  17478  imasip  17479  imasaddfnlem  17486  imasvscafn  17495  isfunc  17825  wunfunc  17862  isnat  17911  natffn  17913  wunnat  17920  fucsect  17936  setcepi  18049  grpinvfval  18948  odfval  19501  dfod2  19533  ghmcyg  19865  gsum2d2lem  19942  gsum2d2  19943  gsumcom2  19944  dmdprd  19969  dprdval  19974  dprdf11  19994  dprd2d2  20015  dpjeq  20030  pgpfac1lem2  20046  pgpfac1lem3  20048  pgpfac1lem4  20049  mptscmfsupp0  20916  00lsp  20970  ocv0  21670  ofco2  22429  tgidm  22958  pptbas  22986  tgrest  23137  iscnp2  23217  ist1-3  23327  discmp  23376  1stcfb  23423  lly1stc  23474  disllycmp  23476  dis1stc  23477  comppfsc  23510  txbas  23545  ptbasfi  23559  ptpjopn  23590  dfac14  23596  ptrescn  23617  xkoptsub  23632  fclsval  23986  ptcmplem2  24031  ptcmplem3  24032  cnextrel  24041  tsmsfbas  24106  ustuqtop  24224  prdsxmetlem  24346  ressprdsds  24349  prdsxmslem2  24507  zcld  24792  xrge0tsms  24813  metdsf  24827  metdsge  24828  minveclem1  25404  minveclem3b  25408  minveclem6  25414  uniioombllem4  25566  uniioombllem6  25568  ismbf3d  25634  i1f1lem  25669  reldv  25850  ellimc2  25857  limcflf  25861  limciun  25874  dvfval  25877  dvrec  25935  dvlipcn  25974  mdegle0  26055  ply1nzb  26101  quotlem  26280  taylfval  26338  ulmdvlem1  26381  ulmdvlem2  26382  ulmdvlem3  26383  psercn  26407  sqff1o  27162  lgsquadlem2  27361  bdayiun  27924  disjxwwlksn  29990  disjxwwlkn  29999  numclwwlk3lem2  30472  grpoidval  30602  grpoidinv2  30604  grpoinv  30614  minvecolem1  30963  minvecolem5  30970  minvecolem6  30971  adjbdln  32172  dfcnv2  32766  intimafv  32802  rexdiv  33003  gsumpart  33142  xrge0tsmsd  33152  fedgmullem2  33793  irngval  33848  rspectopn  34030  zarcls  34037  zartopn  34038  esumnul  34211  esum0  34212  hasheuni  34248  esum2d  34256  ldgenpisyslem3  34328  measvuni  34377  measdivcstALTV  34388  ddemeas  34399  carsgclctunlem2  34482  eulerpartlemgs2  34543  probfinmeasbALTV  34592  0rrv  34614  signsplypnf  34713  signsply0  34714  hgt750lemb  34819  bnj226  34896  bnj98  35028  bnj517  35046  bnj893  35089  bnj1137  35156  rankval4b  35262  rankfilimbi  35263  fineqvnttrclse  35287  tz9.1regs  35297  subfacf  35376  subfacp1lem6  35386  cvmsss2  35475  cvmliftlem1  35486  ixpeq12i  36402  ttciunun  36712  bj-rabtr  37256  bj-axseprep  37400  relowlssretop  37696  fin2so  37945  matunitlindflem1  37954  ptrest  37957  poimirlem23  37981  poimirlem24  37982  poimirlem27  37985  poimirlem30  37988  poimirlem32  37990  cnambfre  38006  upixp  38067  0totbnd  38111  prdsbnd  38131  prdstotbnd  38132  cntotbnd  38134  rrnequiv  38173  ac6s6  38510  dmsucmap  38806  disjimeceqim  39142  cdlemefrs32fva  40863  cdlemkid5  41398  cdlemk56  41434  dihf11lem  41729  addinvcom  42881  0dioph  43227  vdioph  43228  pw2f1ocnv  43486  pwinfi  44012  eliunov2  44127  fvmptiunrelexplb0d  44132  fvmptiunrelexplb1d  44134  iunrelexp0  44150  ntrrn  44570  dssmapntrcls  44576  mnurndlem1  44729  rankrelp  45408  0elaxnul  45431  prclaxpr  45433  uniclaxun  45434  omssaxinf2  45436  wessf1ornlem  45636  axccdom  45672  fnmptif  45715  fsumiunss  46026  limcdm0  46069  liminfval2  46217  liminflelimsuplem  46224  cnrefiisplem  46278  0cnf  46326  dvsinax  46362  ioodvbdlimc1lem2  46381  ioodvbdlimc2lem  46383  dvnprodlem3  46397  iblempty  46414  fourierdlem89  46644  fourierdlem91  46646  fourierdlem100  46655  fourierdlem108  46663  fourierdlem112  46667  salexct3  46791  salgensscntex  46793  omeiunle  46966  0ome  46978  hoissrrn  46998  ovn0  47015  hoissrrn2  47027  hspmbl  47078  ovolval5lem2  47102  iunhoiioolem  47124  vonioolem2  47130  vonicclem2  47133  smflimlem1  47220  smfsuplem1  47260  smfinflem  47266  smflimsuplem1  47269  smflimsuplem2  47270  smflimsuplem3  47271  smflimsuplem4  47272  smflimsuplem5  47273  smflimsuplem7  47275  smfliminflem  47279  nthrucw  47335  ralndv2  47569  iccelpart  47908  eliunxp2  48825  1arymaptf1  49133  iinxp  49321  iinfssclem2  49545  iinfssclem3  49546  iinfssc  49547  imasubclem1  49594