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

Theorem rgenw 2953
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 2951 1 𝑥𝐴 𝜑
Colors of variables: wff setvar class
Syntax hints:  wcel 2030  wral 2941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762
This theorem depends on definitions:  df-bi 197  df-ral 2946
This theorem is referenced by:  rgen2w  2954  reuss  3941  reuun1  3942  rabnc  3995  riinrab  4628  0disj  4677  iinexg  4854  epse  5126  xpiindi  5290  eliunxp  5292  opeliunxp2  5293  elrnmpti  5408  cnviin  5710  fnmpti  6060  eqfnfv  6351  mptexgf  6526  eufnfv  6531  mpt2eq12  6757  porpss  6983  iunex  7189  abrexex2  7190  mpt2ex  7292  suppssov1  7372  suppssfv  7376  opeliunxp2f  7381  onnseq  7486  ixpssmap  7984  boxcutc  7993  nneneq  8184  finsschain  8314  dfom3  8582  cantnfdm  8599  rankuni2b  8754  rankval4  8768  alephf1  8946  dfac4  8983  dfacacn  9001  infmap2  9078  cfeq0  9116  fin23lem28  9200  axdc2lem  9308  axcclem  9317  ac6  9340  iundom  9402  konigthlem  9428  iunctb  9434  tskmid  9700  supaddc  11028  supadd  11029  supmul1  11030  supmullem2  11032  supmul  11033  uzf  11728  seqof  12898  hashbclem  13274  wrdexg  13347  rlimclim1  14320  fsumcom2  14549  fsumcom2OLD  14550  ackbijnn  14604  fprodcom2  14758  fprodcom2OLD  14759  lcmf0  15394  phisum  15542  sumhash  15647  ramcl  15780  prdsval  16162  prdsbas  16164  prdshom  16174  imasplusg  16224  imasmulr  16225  imasvsca  16227  imasip  16228  imasaddfnlem  16235  imasvscafn  16244  isfunc  16571  wunfunc  16606  isnat  16654  natffn  16656  wunnat  16663  fucsect  16679  setcepi  16785  dfod2  18027  ghmcyg  18343  gsum2d2lem  18418  gsum2d2  18419  gsumcom2  18420  dmdprd  18443  dprdval  18448  dprdf11  18468  dprd2d2  18489  dpjeq  18504  pgpfac1lem2  18520  pgpfac1lem3  18522  pgpfac1lem4  18523  mptscmfsupp0  18976  00lsp  19029  ocv0  20069  ofco2  20305  tgidm  20832  pptbas  20860  tgrest  21011  iscnp2  21091  ist1-3  21201  discmp  21249  1stcfb  21296  lly1stc  21347  disllycmp  21349  dis1stc  21350  comppfsc  21383  txbas  21418  ptbasfi  21432  ptpjopn  21463  dfac14  21469  ptrescn  21490  xkoptsub  21505  fclsval  21859  ptcmplem2  21904  ptcmplem3  21905  cnextrel  21914  tsmsfbas  21978  ustuqtop  22097  prdsxmetlem  22220  ressprdsds  22223  prdsxmslem2  22381  zcld  22663  xrge0tsms  22684  metdsf  22698  metdsge  22699  minveclem1  23241  minveclem3b  23245  minveclem6  23251  uniioombllem4  23400  uniioombllem6  23402  ismbf3d  23466  i1f1lem  23501  reldv  23679  ellimc2  23686  limcflf  23690  limciun  23703  dvfval  23706  dvrec  23763  dvlipcn  23802  mdegle0  23882  ply1nzb  23927  quotlem  24100  taylfval  24158  ulmdvlem1  24199  ulmdvlem2  24200  ulmdvlem3  24201  psercn  24225  sqff1o  24953  lgsquadlem2  25151  disjxwwlksn  26867  wwlksnfi  26869  disjxwwlkn  26876  numclwwlk3lem  27371  grpoidval  27495  grpoidinv2  27497  grpoinv  27507  minvecolem1  27858  minvecolem5  27865  minvecolem6  27866  adjbdln  29070  dfcnv2  29604  rexdiv  29762  xrge0tsmsd  29913  esumnul  30238  esum0  30239  hasheuni  30275  esum2d  30283  ldgenpisyslem3  30356  measvuni  30405  measdivcstOLD  30415  ddemeas  30427  carsgclctunlem2  30509  eulerpartlemgs2  30570  probfinmeasbOLD  30618  0rrv  30641  signsplypnf  30755  signsply0  30756  hgt750lemb  30862  bnj226  30928  bnj98  31063  bnj517  31081  bnj893  31124  bnj1137  31189  subfacf  31283  subfacp1lem6  31293  cvmsss2  31382  cvmliftlem1  31393  nulssgt  32034  bj-rabtr  33051  bj-rabtrALTALT  33053  relowlssretop  33341  fin2so  33526  matunitlindflem1  33535  ptrest  33538  poimirlem23  33562  poimirlem24  33563  poimirlem27  33566  poimirlem30  33569  poimirlem32  33571  cnambfre  33588  upixp  33654  0totbnd  33702  prdsbnd  33722  prdstotbnd  33723  cntotbnd  33725  rrnequiv  33764  ac6s6  34110  cdlemefrs32fva  36005  cdlemkid5  36540  cdlemk56  36576  dihf11lem  36872  0dioph  37659  vdioph  37660  rmxyelqirr  37792  pw2f1ocnv  37921  pwinfi  38186  eliunov2  38288  fvmptiunrelexplb0d  38293  fvmptiunrelexplb1d  38295  iunrelexp0  38311  ntrrn  38737  dssmapntrcls  38743  wessf1ornlem  39685  axccdom  39730  mpteq1df  39757  fsumiunss  40125  limcdm0  40168  liminfval2  40318  liminflelimsuplem  40325  cnrefiisplem  40373  0cnf  40408  dvsinax  40445  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  dvnprodlem3  40481  mbf0  40491  iblempty  40499  fourierdlem89  40730  fourierdlem91  40732  fourierdlem100  40741  fourierdlem108  40749  fourierdlem112  40753  salexct3  40878  salgensscntex  40880  omeiunle  41052  0ome  41064  hoissrrn  41084  ovn0  41101  hoissrrn2  41113  hspmbl  41164  ovolval5lem2  41188  ovolval5lem3  41189  iunhoiioolem  41210  vonioolem2  41216  vonicclem2  41219  smflimlem1  41300  smfsuplem1  41338  smfinflem  41344  smflimsuplem1  41347  smflimsuplem2  41348  smflimsuplem3  41349  smflimsuplem4  41350  smflimsuplem5  41351  smflimsuplem7  41353  smfliminflem  41357  iccelpart  41694  eliunxp2  42437
  Copyright terms: Public domain W3C validator