Theorem rgenw 3055

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

Syntax hints:   ∈ wcel 2114  ∀wral 3051

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 3052

This theorem is referenced by:  rgen2w  3056  reuss  4267  reuun1  4268  rabnc  4331  riinrab  5026  0disj  5078  iinexg  5289  epse  5613  xpiindi  5790  eliunxp  5792  opeliunxp2  5793  elrnmpti  5917  cnviin  6250  fnmpti  6641  eqfnfv  6983  eufnfv  7184  mpoeq12  7440  porpss  7681  iunex  7921  abrexex2  7922  mpoex  8032  suppssov1  8147  suppssov2  8148  suppssfv  8152  opeliunxp2f  8160  onnseq  8284  ixpssmap  8880  boxcutc  8889  nneneq  9140  finsschain  9269  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  12123  supadd  12124  supmul1  12125  supmullem2  12127  supmul  12128  uzf  12791  seqof  14021  hashbclem  14414  rlimclim1  15507  fsumcom2  15736  ackbijnn  15793  fprodcom2  15949  lcmf0  16603  phisum  16761  sumhash  16867  ramcl  17000  prdsvallem  17417  prdsval  17418  prdsbas  17420  prdshom  17430  imasplusg  17481  imasmulr  17482  imasvsca  17484  imasip  17485  imasaddfnlem  17492  imasvscafn  17501  isfunc  17831  wunfunc  17868  isnat  17917  natffn  17919  wunnat  17926  fucsect  17942  setcepi  18055  grpinvfval  18954  odfval  19507  dfod2  19539  ghmcyg  19871  gsum2d2lem  19948  gsum2d2  19949  gsumcom2  19950  dmdprd  19975  dprdval  19980  dprdf11  20000  dprd2d2  20021  dpjeq  20036  pgpfac1lem2  20052  pgpfac1lem3  20054  pgpfac1lem4  20055  mptscmfsupp0  20922  00lsp  20976  ocv0  21657  ofco2  22416  tgidm  22945  pptbas  22973  tgrest  23124  iscnp2  23204  ist1-3  23314  discmp  23363  1stcfb  23410  lly1stc  23461  disllycmp  23463  dis1stc  23464  comppfsc  23497  txbas  23532  ptbasfi  23546  ptpjopn  23577  dfac14  23583  ptrescn  23604  xkoptsub  23619  fclsval  23973  ptcmplem2  24018  ptcmplem3  24019  cnextrel  24028  tsmsfbas  24093  ustuqtop  24211  prdsxmetlem  24333  ressprdsds  24336  prdsxmslem2  24494  zcld  24779  xrge0tsms  24800  metdsf  24814  metdsge  24815  minveclem1  25391  minveclem3b  25395  minveclem6  25401  uniioombllem4  25553  uniioombllem6  25555  ismbf3d  25621  i1f1lem  25656  reldv  25837  ellimc2  25844  limcflf  25848  limciun  25861  dvfval  25864  dvrec  25922  dvlipcn  25961  mdegle0  26042  ply1nzb  26088  quotlem  26266  taylfval  26324  ulmdvlem1  26365  ulmdvlem2  26366  ulmdvlem3  26367  psercn  26391  sqff1o  27145  lgsquadlem2  27344  bdayiun  27907  disjxwwlksn  29972  disjxwwlkn  29981  numclwwlk3lem2  30454  grpoidval  30584  grpoidinv2  30586  grpoinv  30596  minvecolem1  30945  minvecolem5  30952  minvecolem6  30953  adjbdln  32154  dfcnv2  32748  intimafv  32784  rexdiv  32985  gsumpart  33124  xrge0tsmsd  33134  fedgmullem2  33774  irngval  33829  rspectopn  34011  zarcls  34018  zartopn  34019  esumnul  34192  esum0  34193  hasheuni  34229  esum2d  34237  ldgenpisyslem3  34309  measvuni  34358  measdivcstALTV  34369  ddemeas  34380  carsgclctunlem2  34463  eulerpartlemgs2  34524  probfinmeasbALTV  34573  0rrv  34595  signsplypnf  34694  signsply0  34695  hgt750lemb  34800  bnj226  34877  bnj98  35009  bnj517  35027  bnj893  35070  bnj1137  35137  rankval4b  35243  rankfilimbi  35244  fineqvnttrclse  35268  tz9.1regs  35278  subfacf  35357  subfacp1lem6  35367  cvmsss2  35456  cvmliftlem1  35467  ixpeq12i  36383  ttciunun  36693  bj-rabtr  37237  bj-axseprep  37381  relowlssretop  37679  fin2so  37928  matunitlindflem1  37937  ptrest  37940  poimirlem23  37964  poimirlem24  37965  poimirlem27  37968  poimirlem30  37971  poimirlem32  37973  cnambfre  37989  upixp  38050  0totbnd  38094  prdsbnd  38114  prdstotbnd  38115  cntotbnd  38117  rrnequiv  38156  ac6s6  38493  dmsucmap  38789  disjimeceqim  39125  cdlemefrs32fva  40846  cdlemkid5  41381  cdlemk56  41417  dihf11lem  41712  addinvcom  42864  0dioph  43210  vdioph  43211  pw2f1ocnv  43465  pwinfi  43991  eliunov2  44106  fvmptiunrelexplb0d  44111  fvmptiunrelexplb1d  44113  iunrelexp0  44129  ntrrn  44549  dssmapntrcls  44555  mnurndlem1  44708  rankrelp  45387  0elaxnul  45410  prclaxpr  45412  uniclaxun  45413  omssaxinf2  45415  wessf1ornlem  45615  axccdom  45651  fnmptif  45694  fsumiunss  46005  limcdm0  46048  liminfval2  46196  liminflelimsuplem  46203  cnrefiisplem  46257  0cnf  46305  dvsinax  46341  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  dvnprodlem3  46376  iblempty  46393  fourierdlem89  46623  fourierdlem91  46625  fourierdlem100  46634  fourierdlem108  46642  fourierdlem112  46646  salexct3  46770  salgensscntex  46772  omeiunle  46945  0ome  46957  hoissrrn  46977  ovn0  46994  hoissrrn2  47006  hspmbl  47057  ovolval5lem2  47081  iunhoiioolem  47103  vonioolem2  47109  vonicclem2  47112  smflimlem1  47199  smfsuplem1  47239  smfinflem  47245  smflimsuplem1  47248  smflimsuplem2  47249  smflimsuplem3  47250  smflimsuplem4  47251  smflimsuplem5  47252  smflimsuplem7  47254  smfliminflem  47258  nthrucw  47316  ralndv2  47554  iccelpart  47893  eliunxp2  48810  1arymaptf1  49118  iinxp  49306  iinfssclem2  49530  iinfssclem3  49531  iinfssc  49532  imasubclem1  49579