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

Theorem rgenw 2907
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 2905 1 𝑥𝐴 𝜑
Colors of variables: wff setvar class
Syntax hints:  wcel 1976  wral 2895
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712
This theorem depends on definitions:  df-bi 195  df-ral 2900
This theorem is referenced by:  rgen2w  2908  reuss  3866  reuun1  3867  rabnc  3915  riinrab  4526  0disj  4569  iinexg  4746  epse  5011  xpiindi  5167  eliunxp  5169  opeliunxp2  5170  elrnmpti  5284  cnviin  5575  fnmpti  5921  eqfnfv  6204  eufnfv  6373  mpt2eq12  6591  porpss  6816  iunex  7016  mpt2ex  7113  suppssov1  7191  suppssfv  7195  opeliunxp2f  7200  onnseq  7305  ixpssmap  7805  boxcutc  7814  nneneq  8005  finsschain  8133  dfom3  8404  cantnfdm  8421  rankuni2b  8576  rankval4  8590  alephf1  8768  dfac4  8805  dfacacn  8823  infmap2  8900  cfeq0  8938  fin23lem28  9022  axdc2lem  9130  axcclem  9139  ac6  9162  iundom  9220  konigthlem  9246  iunctb  9252  tskmid  9518  supaddc  10837  supadd  10838  supmul1  10839  supmullem2  10841  supmul  10842  uzf  11522  seqof  12675  hashbclem  13045  wrdexg  13116  rlimclim1  14070  fsumcom2  14293  fsumcom2OLD  14294  ackbijnn  14345  fprodcom2  14499  fprodcom2OLD  14500  lcmf0  15131  phisum  15279  sumhash  15384  ramcl  15517  prdsval  15884  prdsbas  15886  prdshom  15896  imasplusg  15946  imasmulr  15947  imasvsca  15949  imasip  15950  imasaddfnlem  15957  imasvscafn  15966  isfunc  16293  wunfunc  16328  isnat  16376  natffn  16378  wunnat  16385  fucsect  16401  setcepi  16507  dfod2  17750  ghmcyg  18066  gsum2d2lem  18141  gsum2d2  18142  gsumcom2  18143  dmdprd  18166  dprdval  18171  dprdf11  18191  dprd2d2  18212  dpjeq  18227  pgpfac1lem2  18243  pgpfac1lem3  18245  pgpfac1lem4  18246  mptscmfsupp0  18697  00lsp  18748  ocv0  19782  ofco2  20018  tgidm  20537  pptbas  20564  tgrest  20715  iscnp2  20795  ist1-3  20905  discmp  20953  1stcfb  21000  lly1stc  21051  disllycmp  21053  dis1stc  21054  comppfsc  21087  txbas  21122  ptbasfi  21136  ptpjopn  21167  dfac14  21173  ptrescn  21194  xkoptsub  21209  fclsval  21564  ptcmplem2  21609  ptcmplem3  21610  cnextrel  21619  tsmsfbas  21683  ustuqtop  21802  prdsxmetlem  21924  ressprdsds  21927  prdsxmslem2  22085  zcld  22356  xrge0tsms  22377  metdsf  22390  metdsge  22391  minveclem1  22920  minveclem3b  22924  minveclem6  22930  uniioombllem4  23077  uniioombllem6  23079  ismbf3d  23144  i1f1lem  23179  reldv  23357  ellimc2  23364  limcflf  23368  limciun  23381  dvfval  23384  dvrec  23441  dvlipcn  23478  mdegle0  23558  ply1nzb  23603  quotlem  23776  taylfval  23834  ulmdvlem1  23875  ulmdvlem2  23876  ulmdvlem3  23877  psercn  23901  sqff1o  24625  lgsquadlem2  24823  cusgrasizeindslem1  25768  disjxwwlks  26030  wwlknfi  26032  disjxwwlkn  26039  grpoidval  26517  grpoidinv2  26519  grpoinv  26529  minvecolem1  26920  minvecolem5  26927  minvecolem6  26928  adjbdln  28132  rmoeqALT  28517  mptexgf  28615  dfcnv2  28665  rexdiv  28771  xrge0tsmsd  28922  esumnul  29243  esum0  29244  hasheuni  29280  esum2d  29288  ldgenpisyslem3  29361  measvuni  29410  measdivcstOLD  29420  ddemeas  29432  carsgclctunlem2  29514  eulerpartlemgs2  29575  probfinmeasbOLD  29623  0rrv  29646  signsplypnf  29759  signsply0  29760  bnj226  29862  bnj98  29997  bnj517  30015  bnj893  30058  bnj1137  30123  subfacf  30217  subfacp1lem6  30227  cvmsss2  30316  cvmliftlem1  30327  bj-rabtr  31914  bj-rabtrALTALT  31916  relowlssretop  32183  fin2so  32362  matunitlindflem1  32371  ptrest  32374  poimirlem23  32398  poimirlem24  32399  poimirlem27  32402  poimirlem30  32405  poimirlem32  32407  cnambfre  32424  upixp  32490  0totbnd  32538  prdsbnd  32558  prdstotbnd  32559  cntotbnd  32561  rrnequiv  32600  ac6s6  32946  cdlemefrs32fva  34502  cdlemkid5  35037  cdlemk56  35073  dihf11lem  35369  0dioph  36156  vdioph  36157  rmxyelqirr  36289  pw2f1ocnv  36418  pwinfi  36684  eliunov2  36786  fvmptiunrelexplb0d  36791  fvmptiunrelexplb1d  36793  iunrelexp0  36809  ntrrn  37236  dssmapntrcls  37242  wessf1ornlem  38162  axccdom  38207  fsumiunss  38439  limcdm0  38482  0cnf  38559  dvsinax  38598  ioodvbdlimc1lem2  38619  ioodvbdlimc2lem  38621  dvnprodlem3  38635  mbf0  38646  iblempty  38654  fourierdlem89  38885  fourierdlem91  38887  fourierdlem100  38896  fourierdlem108  38904  fourierdlem112  38908  salexct3  39033  salgensscntex  39035  omeiunle  39204  0ome  39216  hoissrrn  39236  ovn0  39253  hoissrrn2  39265  hspmbl  39316  ovolval5lem2  39340  ovolval5lem3  39341  iunhoiioolem  39363  vonioolem2  39369  vonicclem2  39372  smflimlem1  39454  iccelpart  39769  disjxwwlksn  41105  wwlksnfi  41107  av-disjxwwlkn  41114  eliunxp2  41900
  Copyright terms: Public domain W3C validator