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  4281  reuun1  4282  rabnc  4345  riinrab  5041  0disj  5093  iinexg  5295  epse  5614  xpiindi  5792  eliunxp  5794  opeliunxp2  5795  elrnmpti  5919  cnviin  6252  fnmpti  6643  eqfnfv  6985  eufnfv  7185  mpoeq12  7441  porpss  7682  iunex  7922  abrexex2  7923  mpoex  8033  suppssov1  8149  suppssov2  8150  suppssfv  8154  opeliunxp2f  8162  onnseq  8286  ixpssmap  8882  boxcutc  8891  nneneq  9142  finsschain  9271  dfom3  9568  cantnfdm  9585  rankuni2b  9777  rankval4  9791  alephf1  10007  dfac4  10044  dfacacn  10064  infmap2  10139  cfeq0  10178  fin23lem28  10262  axdc2lem  10370  axcclem  10379  ac6  10402  iundom  10464  konigthlem  10491  iunctb  10497  tskmid  10763  supaddc  12121  supadd  12122  supmul1  12123  supmullem2  12125  supmul  12126  uzf  12766  seqof  13994  hashbclem  14387  rlimclim1  15480  fsumcom2  15709  ackbijnn  15763  fprodcom2  15919  lcmf0  16573  phisum  16730  sumhash  16836  ramcl  16969  prdsvallem  17386  prdsval  17387  prdsbas  17389  prdshom  17399  imasplusg  17450  imasmulr  17451  imasvsca  17453  imasip  17454  imasaddfnlem  17461  imasvscafn  17470  isfunc  17800  wunfunc  17837  isnat  17886  natffn  17888  wunnat  17895  fucsect  17911  setcepi  18024  grpinvfval  18920  odfval  19473  dfod2  19505  ghmcyg  19837  gsum2d2lem  19914  gsum2d2  19915  gsumcom2  19916  dmdprd  19941  dprdval  19946  dprdf11  19966  dprd2d2  19987  dpjeq  20002  pgpfac1lem2  20018  pgpfac1lem3  20020  pgpfac1lem4  20021  mptscmfsupp0  20890  00lsp  20944  ocv0  21644  ofco2  22407  tgidm  22936  pptbas  22964  tgrest  23115  iscnp2  23195  ist1-3  23305  discmp  23354  1stcfb  23401  lly1stc  23452  disllycmp  23454  dis1stc  23455  comppfsc  23488  txbas  23523  ptbasfi  23537  ptpjopn  23568  dfac14  23574  ptrescn  23595  xkoptsub  23610  fclsval  23964  ptcmplem2  24009  ptcmplem3  24010  cnextrel  24019  tsmsfbas  24084  ustuqtop  24202  prdsxmetlem  24324  ressprdsds  24327  prdsxmslem2  24485  zcld  24770  xrge0tsms  24791  metdsf  24805  metdsge  24806  minveclem1  25392  minveclem3b  25396  minveclem6  25402  uniioombllem4  25555  uniioombllem6  25557  ismbf3d  25623  i1f1lem  25658  reldv  25839  ellimc2  25846  limcflf  25850  limciun  25863  dvfval  25866  dvrec  25927  dvlipcn  25967  mdegle0  26050  ply1nzb  26096  quotlem  26276  taylfval  26334  ulmdvlem1  26377  ulmdvlem2  26378  ulmdvlem3  26379  psercn  26404  sqff1o  27160  lgsquadlem2  27360  bdayiun  27923  disjxwwlksn  29989  disjxwwlkn  29998  numclwwlk3lem2  30471  grpoidval  30601  grpoidinv2  30603  grpoinv  30613  minvecolem1  30962  minvecolem5  30969  minvecolem6  30970  adjbdln  32171  dfcnv2  32765  intimafv  32801  rexdiv  33018  gsumpart  33157  xrge0tsmsd  33167  fedgmullem2  33808  irngval  33863  rspectopn  34045  zarcls  34052  zartopn  34053  esumnul  34226  esum0  34227  hasheuni  34263  esum2d  34271  ldgenpisyslem3  34343  measvuni  34392  measdivcstALTV  34403  ddemeas  34414  carsgclctunlem2  34497  eulerpartlemgs2  34558  probfinmeasbALTV  34607  0rrv  34629  signsplypnf  34728  signsply0  34729  hgt750lemb  34834  bnj226  34911  bnj98  35043  bnj517  35061  bnj893  35104  bnj1137  35171  rankval4b  35277  rankfilimbi  35278  fineqvnttrclse  35302  tz9.1regs  35312  subfacf  35391  subfacp1lem6  35401  cvmsss2  35490  cvmliftlem1  35501  ixpeq12i  36417  bj-rabtr  37178  bj-axseprep  37322  relowlssretop  37618  fin2so  37858  matunitlindflem1  37867  ptrest  37870  poimirlem23  37894  poimirlem24  37895  poimirlem27  37898  poimirlem30  37901  poimirlem32  37903  cnambfre  37919  upixp  37980  0totbnd  38024  prdsbnd  38044  prdstotbnd  38045  cntotbnd  38047  rrnequiv  38086  ac6s6  38423  dmsucmap  38719  disjimeceqim  39055  cdlemefrs32fva  40776  cdlemkid5  41311  cdlemk56  41347  dihf11lem  41642  addinvcom  42802  0dioph  43135  vdioph  43136  pw2f1ocnv  43394  pwinfi  43920  eliunov2  44035  fvmptiunrelexplb0d  44040  fvmptiunrelexplb1d  44042  iunrelexp0  44058  ntrrn  44478  dssmapntrcls  44484  mnurndlem1  44637  rankrelp  45316  0elaxnul  45339  prclaxpr  45341  uniclaxun  45342  omssaxinf2  45344  wessf1ornlem  45544  axccdom  45580  fnmptif  45623  fsumiunss  45935  limcdm0  45978  liminfval2  46126  liminflelimsuplem  46133  cnrefiisplem  46187  0cnf  46235  dvsinax  46271  ioodvbdlimc1lem2  46290  ioodvbdlimc2lem  46292  dvnprodlem3  46306  iblempty  46323  fourierdlem89  46553  fourierdlem91  46555  fourierdlem100  46564  fourierdlem108  46572  fourierdlem112  46576  salexct3  46700  salgensscntex  46702  omeiunle  46875  0ome  46887  hoissrrn  46907  ovn0  46924  hoissrrn2  46936  hspmbl  46987  ovolval5lem2  47011  iunhoiioolem  47033  vonioolem2  47039  vonicclem2  47042  smflimlem1  47129  smfsuplem1  47169  smfinflem  47175  smflimsuplem1  47178  smflimsuplem2  47179  smflimsuplem3  47180  smflimsuplem4  47181  smflimsuplem5  47182  smflimsuplem7  47184  smfliminflem  47188  nthrucw  47244  ralndv2  47466  iccelpart  47793  eliunxp2  48694  1arymaptf1  49002  iinxp  49190  iinfssclem2  49414  iinfssclem3  49415  iinfssc  49416  imasubclem1  49463