Theorem rgenw 3152

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

Syntax hints:   ∈ wcel 2114  ∀wral 3140

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

This theorem depends on definitions:  df-bi 209  df-ral 3145

This theorem is referenced by:  rgen2w  3153  reuss  4286  reuun1  4287  rabnc  4343  riinrab  5008  0disj  5060  iinexg  5246  epse  5540  xpiindi  5708  eliunxp  5710  opeliunxp2  5711  elrnmpti  5834  cnviin  6139  fnmpti  6493  eqfnfv  6804  mptexgf  6987  eufnfv  6993  mpoeq12  7229  porpss  7455  iunex  7671  abrexex2  7672  mpoex  7779  suppssov1  7864  suppssfv  7868  opeliunxp2f  7878  onnseq  7983  ixpssmap  8498  boxcutc  8507  nneneq  8702  finsschain  8833  dfom3  9112  cantnfdm  9129  rankuni2b  9284  rankval4  9298  alephf1  9513  dfac4  9550  dfacacn  9569  infmap2  9642  cfeq0  9680  fin23lem28  9764  axdc2lem  9872  axcclem  9881  ac6  9904  iundom  9966  konigthlem  9992  iunctb  9998  tskmid  10264  supaddc  11610  supadd  11611  supmul1  11612  supmullem2  11614  supmul  11615  uzf  12249  seqof  13430  hashbclem  13813  wrdexgOLD  13875  rlimclim1  14904  fsumcom2  15131  ackbijnn  15185  fprodcom2  15340  lcmf0  15980  phisum  16129  sumhash  16234  ramcl  16367  prdsval  16730  prdsbas  16732  prdshom  16742  imasplusg  16792  imasmulr  16793  imasvsca  16795  imasip  16796  imasaddfnlem  16803  imasvscafn  16812  isfunc  17136  wunfunc  17171  isnat  17219  natffn  17221  wunnat  17228  fucsect  17244  setcepi  17350  grpinvfval  18144  odfval  18662  dfod2  18693  ghmcyg  19018  gsum2d2lem  19095  gsum2d2  19096  gsumcom2  19097  dmdprd  19122  dprdval  19127  dprdf11  19147  dprd2d2  19168  dpjeq  19183  pgpfac1lem2  19199  pgpfac1lem3  19201  pgpfac1lem4  19202  mptscmfsupp0  19701  00lsp  19755  ocv0  20823  ofco2  21062  tgidm  21590  pptbas  21618  tgrest  21769  iscnp2  21849  ist1-3  21959  discmp  22008  1stcfb  22055  lly1stc  22106  disllycmp  22108  dis1stc  22109  comppfsc  22142  txbas  22177  ptbasfi  22191  ptpjopn  22222  dfac14  22228  ptrescn  22249  xkoptsub  22264  fclsval  22618  ptcmplem2  22663  ptcmplem3  22664  cnextrel  22673  tsmsfbas  22738  ustuqtop  22857  prdsxmetlem  22980  ressprdsds  22983  prdsxmslem2  23141  zcld  23423  xrge0tsms  23444  metdsf  23458  metdsge  23459  minveclem1  24029  minveclem3b  24033  minveclem6  24039  uniioombllem4  24189  uniioombllem6  24191  ismbf3d  24257  i1f1lem  24292  reldv  24470  ellimc2  24477  limcflf  24481  limciun  24494  dvfval  24497  dvrec  24554  dvlipcn  24593  mdegle0  24673  ply1nzb  24718  quotlem  24891  taylfval  24949  ulmdvlem1  24990  ulmdvlem2  24991  ulmdvlem3  24992  psercn  25016  sqff1o  25761  lgsquadlem2  25959  disjxwwlksn  27684  wwlksnfi  27686  wwlksnfiOLD  27687  disjxwwlkn  27694  numclwwlk3lem2  28165  grpoidval  28292  grpoidinv2  28294  grpoinv  28304  minvecolem1  28653  minvecolem5  28660  minvecolem6  28661  adjbdln  29862  dfcnv2  30424  rexdiv  30604  xrge0tsmsd  30694  fedgmullem2  31028  esumnul  31309  esum0  31310  hasheuni  31346  esum2d  31354  ldgenpisyslem3  31426  measvuni  31475  measdivcstALTV  31486  ddemeas  31497  carsgclctunlem2  31579  eulerpartlemgs2  31640  probfinmeasbALTV  31689  0rrv  31711  signsplypnf  31822  signsply0  31823  hgt750lemb  31929  bnj226  32006  bnj98  32141  bnj517  32159  bnj893  32202  bnj1137  32269  subfacf  32424  subfacp1lem6  32434  cvmsss2  32523  cvmliftlem1  32534  nulssgt  33265  bj-rabtr  34250  relowlssretop  34646  fin2so  34881  matunitlindflem1  34890  ptrest  34893  poimirlem23  34917  poimirlem24  34918  poimirlem27  34921  poimirlem30  34924  poimirlem32  34926  cnambfre  34942  upixp  35006  0totbnd  35053  prdsbnd  35073  prdstotbnd  35074  cntotbnd  35076  rrnequiv  35115  ac6s6  35452  cdlemefrs32fva  37538  cdlemkid5  38073  cdlemk56  38109  dihf11lem  38404  0dioph  39382  vdioph  39383  rmxyelqirr  39514  pw2f1ocnv  39641  pwinfi  39930  eliunov2  40031  fvmptiunrelexplb0d  40036  fvmptiunrelexplb1d  40038  iunrelexp0  40054  ntrrn  40479  dssmapntrcls  40485  mnurndlem1  40624  wessf1ornlem  41452  axccdom  41494  mpteq1df  41513  fsumiunss  41863  limcdm0  41906  liminfval2  42056  liminflelimsuplem  42063  cnrefiisplem  42117  0cnf  42167  dvsinax  42204  ioodvbdlimc1lem2  42224  ioodvbdlimc2lem  42226  dvnprodlem3  42240  iblempty  42257  fourierdlem89  42487  fourierdlem91  42489  fourierdlem100  42498  fourierdlem108  42506  fourierdlem112  42510  salexct3  42632  salgensscntex  42634  omeiunle  42806  0ome  42818  hoissrrn  42838  ovn0  42855  hoissrrn2  42867  hspmbl  42918  ovolval5lem2  42942  ovolval5lem3  42943  iunhoiioolem  42964  vonioolem2  42970  vonicclem2  42973  smflimlem1  43054  smfsuplem1  43092  smfinflem  43098  smflimsuplem1  43101  smflimsuplem2  43102  smflimsuplem3  43103  smflimsuplem4  43104  smflimsuplem5  43105  smflimsuplem7  43107  smfliminflem  43111  ralndv2  43312  iccelpart  43600  eliunxp2  44389