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  27831  disjxwwlksn  29853  disjxwwlkn  29862  numclwwlk3lem2  30332  grpoidval  30461  grpoidinv2  30463  grpoinv  30473  minvecolem1  30822  minvecolem5  30829  minvecolem6  30830  adjbdln  32031  dfcnv2  32627  intimafv  32661  rexdiv  32875  gsumpart  33019  xrge0tsmsd  33024  fedgmullem2  33613  irngval  33668  rspectopn  33850  zarcls  33857  zartopn  33858  esumnul  34031  esum0  34032  hasheuni  34068  esum2d  34076  ldgenpisyslem3  34148  measvuni  34197  measdivcstALTV  34208  ddemeas  34219  carsgclctunlem2  34303  eulerpartlemgs2  34364  probfinmeasbALTV  34413  0rrv  34435  signsplypnf  34534  signsply0  34535  hgt750lemb  34640  bnj226  34717  bnj98  34850  bnj517  34868  bnj893  34911  bnj1137  34978  tz9.1regs  35083  fineqvnttrclse  35093  subfacf  35168  subfacp1lem6  35178  cvmsss2  35267  cvmliftlem1  35278  ixpeq12i  36195  bj-rabtr  36924  relowlssretop  37357  fin2so  37607  matunitlindflem1  37616  ptrest  37619  poimirlem23  37643  poimirlem24  37644  poimirlem27  37647  poimirlem30  37650  poimirlem32  37652  cnambfre  37668  upixp  37729  0totbnd  37773  prdsbnd  37793  prdstotbnd  37794  cntotbnd  37796  rrnequiv  37835  ac6s6  38172  cdlemefrs32fva  40399  cdlemkid5  40934  cdlemk56  40970  dihf11lem  41265  addinvcom  42425  0dioph  42771  vdioph  42772  pw2f1ocnv  43030  pwinfi  43557  eliunov2  43672  fvmptiunrelexplb0d  43677  fvmptiunrelexplb1d  43679  iunrelexp0  43695  ntrrn  44115  dssmapntrcls  44121  mnurndlem1  44274  rankrelp  44954  0elaxnul  44977  prclaxpr  44979  uniclaxun  44980  omssaxinf2  44982  wessf1ornlem  45183  axccdom  45220  fnmptif  45263  fsumiunss  45576  limcdm0  45619  liminfval2  45769  liminflelimsuplem  45776  cnrefiisplem  45830  0cnf  45878  dvsinax  45914  ioodvbdlimc1lem2  45933  ioodvbdlimc2lem  45935  dvnprodlem3  45949  iblempty  45966  fourierdlem89  46196  fourierdlem91  46198  fourierdlem100  46207  fourierdlem108  46215  fourierdlem112  46219  salexct3  46343  salgensscntex  46345  omeiunle  46518  0ome  46530  hoissrrn  46550  ovn0  46567  hoissrrn2  46579  hspmbl  46630  ovolval5lem2  46654  iunhoiioolem  46676  vonioolem2  46682  vonicclem2  46685  smflimlem1  46772  smfsuplem1  46812  smfinflem  46818  smflimsuplem1  46821  smflimsuplem2  46822  smflimsuplem3  46823  smflimsuplem4  46824  smflimsuplem5  46825  smflimsuplem7  46827  smfliminflem  46831  ralndv2  47110  iccelpart  47437  eliunxp2  48338  1arymaptf1  48647  iinxp  48835  iinfssclem2  49060  iinfssclem3  49061  iinfssc  49062  imasubclem1  49109