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

Theorem rgenw 2908
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 2906 1 𝑥𝐴 𝜑
Colors of variables: wff setvar class
Syntax hints:  wcel 1977  wral 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713
This theorem depends on definitions:  df-bi 196  df-ral 2901
This theorem is referenced by:  rgen2w  2909  reuss  3867  reuun1  3868  rabnc  3916  riinrab  4532  0disj  4575  iinexg  4751  epse  5021  xpiindi  5179  eliunxp  5181  opeliunxp2  5182  elrnmpti  5297  cnviin  5589  fnmpti  5935  eqfnfv  6219  eufnfv  6395  mpt2eq12  6613  porpss  6839  iunex  7039  mpt2ex  7136  suppssov1  7214  suppssfv  7218  opeliunxp2f  7223  onnseq  7328  ixpssmap  7828  boxcutc  7837  nneneq  8028  finsschain  8156  dfom3  8427  cantnfdm  8444  rankuni2b  8599  rankval4  8613  alephf1  8791  dfac4  8828  dfacacn  8846  infmap2  8923  cfeq0  8961  fin23lem28  9045  axdc2lem  9153  axcclem  9162  ac6  9185  iundom  9243  konigthlem  9269  iunctb  9275  tskmid  9541  supaddc  10867  supadd  10868  supmul1  10869  supmullem2  10871  supmul  10872  uzf  11566  seqof  12720  hashbclem  13093  wrdexg  13170  rlimclim1  14124  fsumcom2  14347  fsumcom2OLD  14348  ackbijnn  14399  fprodcom2  14553  fprodcom2OLD  14554  lcmf0  15185  phisum  15333  sumhash  15438  ramcl  15571  prdsval  15938  prdsbas  15940  prdshom  15950  imasplusg  16000  imasmulr  16001  imasvsca  16003  imasip  16004  imasaddfnlem  16011  imasvscafn  16020  isfunc  16347  wunfunc  16382  isnat  16430  natffn  16432  wunnat  16439  fucsect  16455  setcepi  16561  dfod2  17804  ghmcyg  18120  gsum2d2lem  18195  gsum2d2  18196  gsumcom2  18197  dmdprd  18220  dprdval  18225  dprdf11  18245  dprd2d2  18266  dpjeq  18281  pgpfac1lem2  18297  pgpfac1lem3  18299  pgpfac1lem4  18300  mptscmfsupp0  18751  00lsp  18802  ocv0  19840  ofco2  20076  tgidm  20595  pptbas  20622  tgrest  20773  iscnp2  20853  ist1-3  20963  discmp  21011  1stcfb  21058  lly1stc  21109  disllycmp  21111  dis1stc  21112  comppfsc  21145  txbas  21180  ptbasfi  21194  ptpjopn  21225  dfac14  21231  ptrescn  21252  xkoptsub  21267  fclsval  21622  ptcmplem2  21667  ptcmplem3  21668  cnextrel  21677  tsmsfbas  21741  ustuqtop  21860  prdsxmetlem  21983  ressprdsds  21986  prdsxmslem2  22144  zcld  22424  xrge0tsms  22445  metdsf  22459  metdsge  22460  minveclem1  23003  minveclem3b  23007  minveclem6  23013  uniioombllem4  23160  uniioombllem6  23162  ismbf3d  23227  i1f1lem  23262  reldv  23440  ellimc2  23447  limcflf  23451  limciun  23464  dvfval  23467  dvrec  23524  dvlipcn  23561  mdegle0  23641  ply1nzb  23686  quotlem  23859  taylfval  23917  ulmdvlem1  23958  ulmdvlem2  23959  ulmdvlem3  23960  psercn  23984  sqff1o  24708  lgsquadlem2  24906  cusgrasizeindslem1  26002  disjxwwlks  26264  wwlknfi  26266  disjxwwlkn  26273  grpoidval  26751  grpoidinv2  26753  grpoinv  26763  minvecolem1  27114  minvecolem5  27121  minvecolem6  27122  adjbdln  28326  rmoeqALT  28711  mptexgf  28809  dfcnv2  28859  rexdiv  28965  xrge0tsmsd  29116  esumnul  29437  esum0  29438  hasheuni  29474  esum2d  29482  ldgenpisyslem3  29555  measvuni  29604  measdivcstOLD  29614  ddemeas  29626  carsgclctunlem2  29708  eulerpartlemgs2  29769  probfinmeasbOLD  29817  0rrv  29840  signsplypnf  29953  signsply0  29954  bnj226  30056  bnj98  30191  bnj517  30209  bnj893  30252  bnj1137  30317  subfacf  30411  subfacp1lem6  30421  cvmsss2  30510  cvmliftlem1  30521  bj-rabtr  32118  bj-rabtrALTALT  32120  relowlssretop  32387  fin2so  32566  matunitlindflem1  32575  ptrest  32578  poimirlem23  32602  poimirlem24  32603  poimirlem27  32606  poimirlem30  32609  poimirlem32  32611  cnambfre  32628  upixp  32694  0totbnd  32742  prdsbnd  32762  prdstotbnd  32763  cntotbnd  32765  rrnequiv  32804  ac6s6  33150  cdlemefrs32fva  34706  cdlemkid5  35241  cdlemk56  35277  dihf11lem  35573  0dioph  36360  vdioph  36361  rmxyelqirr  36493  pw2f1ocnv  36622  pwinfi  36888  eliunov2  36990  fvmptiunrelexplb0d  36995  fvmptiunrelexplb1d  36997  iunrelexp0  37013  ntrrn  37440  dssmapntrcls  37446  wessf1ornlem  38366  axccdom  38411  fsumiunss  38642  limcdm0  38685  0cnf  38762  dvsinax  38801  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  dvnprodlem3  38838  mbf0  38849  iblempty  38857  fourierdlem89  39088  fourierdlem91  39090  fourierdlem100  39099  fourierdlem108  39107  fourierdlem112  39111  salexct3  39236  salgensscntex  39238  omeiunle  39407  0ome  39419  hoissrrn  39439  ovn0  39456  hoissrrn2  39468  hspmbl  39519  ovolval5lem2  39543  ovolval5lem3  39544  iunhoiioolem  39566  vonioolem2  39572  vonicclem2  39575  smflimlem1  39657  iccelpart  39971  disjxwwlksn  41110  wwlksnfi  41112  av-disjxwwlkn  41119  eliunxp2  41905
  Copyright terms: Public domain W3C validator