MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rgenw Structured version   Visualization version   GIF version

Theorem rgenw 3112
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
StepHypRef Expression
1 rgenw.1 . . 3 𝜑
21a1i 11 . 2 (𝑥𝐴𝜑)
32rgen 3110 1 𝑥𝐴 𝜑
Colors of variables: wff setvar class
Syntax hints:  wcel 2156  wral 3096
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877
This theorem depends on definitions:  df-bi 198  df-ral 3101
This theorem is referenced by:  rgen2w  3113  reuss  4109  reuun1  4110  rabnc  4160  riinrab  4788  0disj  4837  iinexg  5016  epse  5294  xpiindi  5459  eliunxp  5461  opeliunxp2  5462  elrnmpti  5577  cnviin  5886  fnmpti  6229  eqfnfv  6529  mptexgf  6706  eufnfv  6712  mpt2eq12  6941  porpss  7167  iunex  7373  abrexex2  7374  mpt2ex  7476  suppssov1  7558  suppssfv  7562  opeliunxp2f  7567  onnseq  7673  ixpssmap  8175  boxcutc  8184  nneneq  8378  finsschain  8508  dfom3  8787  cantnfdm  8804  rankuni2b  8959  rankval4  8973  alephf1  9187  dfac4  9224  dfacacn  9244  infmap2  9321  cfeq0  9359  fin23lem28  9443  axdc2lem  9551  axcclem  9560  ac6  9583  iundom  9645  konigthlem  9671  iunctb  9677  tskmid  9943  supaddc  11271  supadd  11272  supmul1  11273  supmullem2  11275  supmul  11276  uzf  11903  seqof  13077  hashbclem  13449  wrdexg  13522  rlimclim1  14495  fsumcom2  14724  ackbijnn  14778  fprodcom2  14931  lcmf0  15562  phisum  15708  sumhash  15813  ramcl  15946  prdsval  16316  prdsbas  16318  prdshom  16328  imasplusg  16378  imasmulr  16379  imasvsca  16381  imasip  16382  imasaddfnlem  16389  imasvscafn  16398  isfunc  16724  wunfunc  16759  isnat  16807  natffn  16809  wunnat  16816  fucsect  16832  setcepi  16938  dfod2  18178  ghmcyg  18494  gsum2d2lem  18569  gsum2d2  18570  gsumcom2  18571  dmdprd  18595  dprdval  18600  dprdf11  18620  dprd2d2  18641  dpjeq  18656  pgpfac1lem2  18672  pgpfac1lem3  18674  pgpfac1lem4  18675  mptscmfsupp0  19128  00lsp  19184  ocv0  20227  ofco2  20464  tgidm  20994  pptbas  21022  tgrest  21173  iscnp2  21253  ist1-3  21363  discmp  21411  1stcfb  21458  lly1stc  21509  disllycmp  21511  dis1stc  21512  comppfsc  21545  txbas  21580  ptbasfi  21594  ptpjopn  21625  dfac14  21631  ptrescn  21652  xkoptsub  21667  fclsval  22021  ptcmplem2  22066  ptcmplem3  22067  cnextrel  22076  tsmsfbas  22140  ustuqtop  22259  prdsxmetlem  22382  ressprdsds  22385  prdsxmslem2  22543  zcld  22825  xrge0tsms  22846  metdsf  22860  metdsge  22861  minveclem1  23403  minveclem3b  23407  minveclem6  23413  uniioombllem4  23563  uniioombllem6  23565  ismbf3d  23631  i1f1lem  23666  reldv  23844  ellimc2  23851  limcflf  23855  limciun  23868  dvfval  23871  dvrec  23928  dvlipcn  23967  mdegle0  24047  ply1nzb  24092  quotlem  24265  taylfval  24323  ulmdvlem1  24364  ulmdvlem2  24365  ulmdvlem3  24366  psercn  24390  sqff1o  25118  lgsquadlem2  25316  disjxwwlksn  27037  wwlksnfi  27039  disjxwwlkn  27047  numclwwlk3lem2  27568  grpoidval  27692  grpoidinv2  27694  grpoinv  27704  minvecolem1  28054  minvecolem5  28061  minvecolem6  28062  adjbdln  29266  dfcnv2  29799  rexdiv  29955  xrge0tsmsd  30106  esumnul  30431  esum0  30432  hasheuni  30468  esum2d  30476  ldgenpisyslem3  30549  measvuni  30598  measdivcstOLD  30608  ddemeas  30620  carsgclctunlem2  30702  eulerpartlemgs2  30763  probfinmeasbOLD  30811  0rrv  30834  signsplypnf  30948  signsply0  30949  hgt750lemb  31055  bnj226  31121  bnj98  31255  bnj517  31273  bnj893  31316  bnj1137  31381  subfacf  31475  subfacp1lem6  31485  cvmsss2  31574  cvmliftlem1  31585  nulssgt  32225  bj-rabtr  33232  bj-rabtrALTALT  33234  relowlssretop  33522  fin2so  33704  matunitlindflem1  33713  ptrest  33716  poimirlem23  33740  poimirlem24  33741  poimirlem27  33744  poimirlem30  33747  poimirlem32  33749  cnambfre  33765  upixp  33831  0totbnd  33878  prdsbnd  33898  prdstotbnd  33899  cntotbnd  33901  rrnequiv  33940  ac6s6  34285  cdlemefrs32fva  36175  cdlemkid5  36710  cdlemk56  36746  dihf11lem  37041  0dioph  37838  vdioph  37839  rmxyelqirr  37970  pw2f1ocnv  38099  pwinfi  38363  eliunov2  38465  fvmptiunrelexplb0d  38470  fvmptiunrelexplb1d  38472  iunrelexp0  38488  ntrrn  38914  dssmapntrcls  38920  wessf1ornlem  39854  axccdom  39897  mpteq1df  39921  fsumiunss  40281  limcdm0  40324  liminfval2  40474  liminflelimsuplem  40481  cnrefiisplem  40529  0cnf  40564  dvsinax  40601  ioodvbdlimc1lem2  40621  ioodvbdlimc2lem  40623  dvnprodlem3  40637  iblempty  40654  fourierdlem89  40885  fourierdlem91  40887  fourierdlem100  40896  fourierdlem108  40904  fourierdlem112  40908  salexct3  41033  salgensscntex  41035  omeiunle  41207  0ome  41219  hoissrrn  41239  ovn0  41256  hoissrrn2  41268  hspmbl  41319  ovolval5lem2  41343  ovolval5lem3  41344  iunhoiioolem  41365  vonioolem2  41371  vonicclem2  41374  smflimlem1  41455  smfsuplem1  41493  smfinflem  41499  smflimsuplem1  41502  smflimsuplem2  41503  smflimsuplem3  41504  smflimsuplem4  41505  smflimsuplem5  41506  smflimsuplem7  41508  smfliminflem  41512  iccelpart  41938  eliunxp2  42674
  Copyright terms: Public domain W3C validator