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  4278  reuun1  4279  rabnc  4342  riinrab  5033  0disj  5085  iinexg  5287  epse  5601  xpiindi  5778  eliunxp  5780  opeliunxp2  5781  elrnmpti  5904  cnviin  6234  fnmpti  6625  eqfnfv  6965  eufnfv  7165  mpoeq12  7422  porpss  7663  iunex  7903  abrexex2  7904  mpoex  8014  suppssov1  8130  suppssov2  8131  suppssfv  8135  opeliunxp2f  8143  onnseq  8267  ixpssmap  8859  boxcutc  8868  nneneq  9120  finsschain  9249  dfom3  9543  cantnfdm  9560  rankuni2b  9749  rankval4  9763  alephf1  9979  dfac4  10016  dfacacn  10036  infmap2  10111  cfeq0  10150  fin23lem28  10234  axdc2lem  10342  axcclem  10351  ac6  10374  iundom  10436  konigthlem  10462  iunctb  10468  tskmid  10734  supaddc  12092  supadd  12093  supmul1  12094  supmullem2  12096  supmul  12097  uzf  12738  seqof  13966  hashbclem  14359  rlimclim1  15452  fsumcom2  15681  ackbijnn  15735  fprodcom2  15891  lcmf0  16545  phisum  16702  sumhash  16808  ramcl  16941  prdsvallem  17358  prdsval  17359  prdsbas  17361  prdshom  17371  imasplusg  17421  imasmulr  17422  imasvsca  17424  imasip  17425  imasaddfnlem  17432  imasvscafn  17441  isfunc  17771  wunfunc  17808  isnat  17857  natffn  17859  wunnat  17866  fucsect  17882  setcepi  17995  grpinvfval  18857  odfval  19411  dfod2  19443  ghmcyg  19775  gsum2d2lem  19852  gsum2d2  19853  gsumcom2  19854  dmdprd  19879  dprdval  19884  dprdf11  19904  dprd2d2  19925  dpjeq  19940  pgpfac1lem2  19956  pgpfac1lem3  19958  pgpfac1lem4  19959  mptscmfsupp0  20830  00lsp  20884  ocv0  21584  ofco2  22336  tgidm  22865  pptbas  22893  tgrest  23044  iscnp2  23124  ist1-3  23234  discmp  23283  1stcfb  23330  lly1stc  23381  disllycmp  23383  dis1stc  23384  comppfsc  23417  txbas  23452  ptbasfi  23466  ptpjopn  23497  dfac14  23503  ptrescn  23524  xkoptsub  23539  fclsval  23893  ptcmplem2  23938  ptcmplem3  23939  cnextrel  23948  tsmsfbas  24013  ustuqtop  24132  prdsxmetlem  24254  ressprdsds  24257  prdsxmslem2  24415  zcld  24700  xrge0tsms  24721  metdsf  24735  metdsge  24736  minveclem1  25322  minveclem3b  25326  minveclem6  25332  uniioombllem4  25485  uniioombllem6  25487  ismbf3d  25553  i1f1lem  25588  reldv  25769  ellimc2  25776  limcflf  25780  limciun  25793  dvfval  25796  dvrec  25857  dvlipcn  25897  mdegle0  25980  ply1nzb  26026  quotlem  26206  taylfval  26264  ulmdvlem1  26307  ulmdvlem2  26308  ulmdvlem3  26309  psercn  26334  sqff1o  27090  lgsquadlem2  27290  bdayiun  27829  disjxwwlksn  29849  disjxwwlkn  29858  numclwwlk3lem2  30328  grpoidval  30457  grpoidinv2  30459  grpoinv  30469  minvecolem1  30818  minvecolem5  30825  minvecolem6  30826  adjbdln  32027  dfcnv2  32619  intimafv  32653  rexdiv  32866  gsumpart  33010  xrge0tsmsd  33015  fedgmullem2  33597  irngval  33652  rspectopn  33834  zarcls  33841  zartopn  33842  esumnul  34015  esum0  34016  hasheuni  34052  esum2d  34060  ldgenpisyslem3  34132  measvuni  34181  measdivcstALTV  34192  ddemeas  34203  carsgclctunlem2  34287  eulerpartlemgs2  34348  probfinmeasbALTV  34397  0rrv  34419  signsplypnf  34518  signsply0  34519  hgt750lemb  34624  bnj226  34701  bnj98  34834  bnj517  34852  bnj893  34895  bnj1137  34962  tz9.1regs  35067  fineqvnttrclse  35077  subfacf  35152  subfacp1lem6  35162  cvmsss2  35251  cvmliftlem1  35262  ixpeq12i  36179  bj-rabtr  36908  relowlssretop  37341  fin2so  37591  matunitlindflem1  37600  ptrest  37603  poimirlem23  37627  poimirlem24  37628  poimirlem27  37631  poimirlem30  37634  poimirlem32  37636  cnambfre  37652  upixp  37713  0totbnd  37757  prdsbnd  37777  prdstotbnd  37778  cntotbnd  37780  rrnequiv  37819  ac6s6  38156  cdlemefrs32fva  40383  cdlemkid5  40918  cdlemk56  40954  dihf11lem  41249  addinvcom  42409  0dioph  42755  vdioph  42756  pw2f1ocnv  43014  pwinfi  43541  eliunov2  43656  fvmptiunrelexplb0d  43661  fvmptiunrelexplb1d  43663  iunrelexp0  43679  ntrrn  44099  dssmapntrcls  44105  mnurndlem1  44258  rankrelp  44938  0elaxnul  44961  prclaxpr  44963  uniclaxun  44964  omssaxinf2  44966  wessf1ornlem  45167  axccdom  45204  fnmptif  45247  fsumiunss  45560  limcdm0  45603  liminfval2  45753  liminflelimsuplem  45760  cnrefiisplem  45814  0cnf  45862  dvsinax  45898  ioodvbdlimc1lem2  45917  ioodvbdlimc2lem  45919  dvnprodlem3  45933  iblempty  45950  fourierdlem89  46180  fourierdlem91  46182  fourierdlem100  46191  fourierdlem108  46199  fourierdlem112  46203  salexct3  46327  salgensscntex  46329  omeiunle  46502  0ome  46514  hoissrrn  46534  ovn0  46551  hoissrrn2  46563  hspmbl  46614  ovolval5lem2  46638  iunhoiioolem  46660  vonioolem2  46666  vonicclem2  46669  smflimlem1  46756  smfsuplem1  46796  smfinflem  46802  smflimsuplem1  46805  smflimsuplem2  46806  smflimsuplem3  46807  smflimsuplem4  46808  smflimsuplem5  46809  smflimsuplem7  46811  smfliminflem  46815  ralndv2  47094  iccelpart  47421  eliunxp2  48322  1arymaptf1  48631  iinxp  48819  iinfssclem2  49044  iinfssclem3  49045  iinfssc  49046  imasubclem1  49093