Theorem rgenw 3075

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

Syntax hints:   ∈ wcel 2108  ∀wral 3063

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

This theorem depends on definitions:  df-bi 206  df-ral 3068

This theorem is referenced by:  rgen2w  3076  reuss  4247  reuun1  4248  rabnc  4318  riinrab  5009  0disj  5062  iinexg  5260  epse  5563  xpiindi  5733  eliunxp  5735  opeliunxp2  5736  elrnmpti  5858  cnviin  6178  fnmpti  6560  eqfnfv  6891  mptexgf  7080  eufnfv  7087  mpoeq12  7326  porpss  7558  iunex  7784  abrexex2  7785  mpoex  7893  suppssov1  7985  suppssfv  7989  opeliunxp2f  7997  onnseq  8146  ixpssmap  8678  boxcutc  8687  nneneq  8896  finsschain  9056  dfom3  9335  cantnfdm  9352  rankuni2b  9542  rankval4  9556  alephf1  9772  dfac4  9809  dfacacn  9828  infmap2  9905  cfeq0  9943  fin23lem28  10027  axdc2lem  10135  axcclem  10144  ac6  10167  iundom  10229  konigthlem  10255  iunctb  10261  tskmid  10527  supaddc  11872  supadd  11873  supmul1  11874  supmullem2  11876  supmul  11877  uzf  12514  seqof  13708  hashbclem  14092  rlimclim1  15182  fsumcom2  15414  ackbijnn  15468  fprodcom2  15622  lcmf0  16267  phisum  16419  sumhash  16525  ramcl  16658  prdsvallem  17082  prdsval  17083  prdsbas  17085  prdshom  17095  imasplusg  17145  imasmulr  17146  imasvsca  17148  imasip  17149  imasaddfnlem  17156  imasvscafn  17165  isfunc  17495  wunfunc  17530  wunfuncOLD  17531  isnat  17579  natffn  17581  wunnat  17588  wunnatOLD  17589  fucsect  17606  setcepi  17719  grpinvfval  18533  odfval  19055  dfod2  19086  ghmcyg  19412  gsum2d2lem  19489  gsum2d2  19490  gsumcom2  19491  dmdprd  19516  dprdval  19521  dprdf11  19541  dprd2d2  19562  dpjeq  19577  pgpfac1lem2  19593  pgpfac1lem3  19595  pgpfac1lem4  19596  mptscmfsupp0  20103  00lsp  20158  ocv0  20794  ofco2  21508  tgidm  22038  pptbas  22066  tgrest  22218  iscnp2  22298  ist1-3  22408  discmp  22457  1stcfb  22504  lly1stc  22555  disllycmp  22557  dis1stc  22558  comppfsc  22591  txbas  22626  ptbasfi  22640  ptpjopn  22671  dfac14  22677  ptrescn  22698  xkoptsub  22713  fclsval  23067  ptcmplem2  23112  ptcmplem3  23113  cnextrel  23122  tsmsfbas  23187  ustuqtop  23306  prdsxmetlem  23429  ressprdsds  23432  prdsxmslem2  23591  zcld  23882  xrge0tsms  23903  metdsf  23917  metdsge  23918  minveclem1  24493  minveclem3b  24497  minveclem6  24503  uniioombllem4  24655  uniioombllem6  24657  ismbf3d  24723  i1f1lem  24758  reldv  24939  ellimc2  24946  limcflf  24950  limciun  24963  dvfval  24966  dvrec  25024  dvlipcn  25063  mdegle0  25147  ply1nzb  25192  quotlem  25365  taylfval  25423  ulmdvlem1  25464  ulmdvlem2  25465  ulmdvlem3  25466  psercn  25490  sqff1o  26236  lgsquadlem2  26434  disjxwwlksn  28170  wwlksnfi  28172  disjxwwlkn  28179  numclwwlk3lem2  28649  grpoidval  28776  grpoidinv2  28778  grpoinv  28788  minvecolem1  29137  minvecolem5  29144  minvecolem6  29145  adjbdln  30346  dfcnv2  30915  intimafv  30945  rexdiv  31102  gsumpart  31217  xrge0tsmsd  31219  fedgmullem2  31613  rspectopn  31719  zarcls  31726  zartopn  31727  esumnul  31916  esum0  31917  hasheuni  31953  esum2d  31961  ldgenpisyslem3  32033  measvuni  32082  measdivcstALTV  32093  ddemeas  32104  carsgclctunlem2  32186  eulerpartlemgs2  32247  probfinmeasbALTV  32296  0rrv  32318  signsplypnf  32429  signsply0  32430  hgt750lemb  32536  bnj226  32613  bnj98  32747  bnj517  32765  bnj893  32808  bnj1137  32875  subfacf  33037  subfacp1lem6  33047  cvmsss2  33136  cvmliftlem1  33147  bj-rabtr  35045  relowlssretop  35461  fin2so  35691  matunitlindflem1  35700  ptrest  35703  poimirlem23  35727  poimirlem24  35728  poimirlem27  35731  poimirlem30  35734  poimirlem32  35736  cnambfre  35752  upixp  35814  0totbnd  35858  prdsbnd  35878  prdstotbnd  35879  cntotbnd  35881  rrnequiv  35920  ac6s6  36257  cdlemefrs32fva  38341  cdlemkid5  38876  cdlemk56  38912  dihf11lem  39207  addinvcom  40334  0dioph  40516  vdioph  40517  rmxyelqirr  40648  pw2f1ocnv  40775  pwinfi  41060  eliunov2  41176  fvmptiunrelexplb0d  41181  fvmptiunrelexplb1d  41183  iunrelexp0  41199  ntrrn  41621  dssmapntrcls  41627  mnurndlem1  41788  wessf1ornlem  42611  axccdom  42651  mpteq1dfOLD  42669  fsumiunss  43006  limcdm0  43049  liminfval2  43199  liminflelimsuplem  43206  cnrefiisplem  43260  0cnf  43308  dvsinax  43344  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  dvnprodlem3  43379  iblempty  43396  fourierdlem89  43626  fourierdlem91  43628  fourierdlem100  43637  fourierdlem108  43645  fourierdlem112  43649  salexct3  43771  salgensscntex  43773  omeiunle  43945  0ome  43957  hoissrrn  43977  ovn0  43994  hoissrrn2  44006  hspmbl  44057  ovolval5lem2  44081  ovolval5lem3  44082  iunhoiioolem  44103  vonioolem2  44109  vonicclem2  44112  smflimlem1  44193  smfsuplem1  44231  smfinflem  44237  smflimsuplem1  44240  smflimsuplem2  44241  smflimsuplem3  44242  smflimsuplem4  44243  smflimsuplem5  44244  smflimsuplem7  44246  smfliminflem  44250  ralndv2  44485  iccelpart  44773  eliunxp2  45557  1arymaptf1  45876