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

Theorem rgenw 3118
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 3116 1 𝑥𝐴 𝜑
Colors of variables: wff setvar class
Syntax hints:  wcel 2111  wral 3106
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797
This theorem depends on definitions:  df-bi 210  df-ral 3111
This theorem is referenced by:  rgen2w  3119  reuss  4236  reuun1  4237  rabnc  4295  riinrab  4969  0disj  5022  iinexg  5208  epse  5502  xpiindi  5670  eliunxp  5672  opeliunxp2  5673  elrnmpti  5796  cnviin  6105  fnmpti  6463  eqfnfv  6779  mptexgf  6962  eufnfv  6969  mpoeq12  7206  porpss  7433  iunex  7651  abrexex2  7652  mpoex  7760  suppssov1  7845  suppssfv  7849  opeliunxp2f  7859  onnseq  7964  ixpssmap  8479  boxcutc  8488  nneneq  8684  finsschain  8815  dfom3  9094  cantnfdm  9111  rankuni2b  9266  rankval4  9280  alephf1  9496  dfac4  9533  dfacacn  9552  infmap2  9629  cfeq0  9667  fin23lem28  9751  axdc2lem  9859  axcclem  9868  ac6  9891  iundom  9953  konigthlem  9979  iunctb  9985  tskmid  10251  supaddc  11595  supadd  11596  supmul1  11597  supmullem2  11599  supmul  11600  uzf  12234  seqof  13423  hashbclem  13806  rlimclim1  14894  fsumcom2  15121  ackbijnn  15175  fprodcom2  15330  lcmf0  15968  phisum  16117  sumhash  16222  ramcl  16355  prdsval  16720  prdsbas  16722  prdshom  16732  imasplusg  16782  imasmulr  16783  imasvsca  16785  imasip  16786  imasaddfnlem  16793  imasvscafn  16802  isfunc  17126  wunfunc  17161  isnat  17209  natffn  17211  wunnat  17218  fucsect  17234  setcepi  17340  grpinvfval  18134  odfval  18652  dfod2  18683  ghmcyg  19009  gsum2d2lem  19086  gsum2d2  19087  gsumcom2  19088  dmdprd  19113  dprdval  19118  dprdf11  19138  dprd2d2  19159  dpjeq  19174  pgpfac1lem2  19190  pgpfac1lem3  19192  pgpfac1lem4  19193  mptscmfsupp0  19692  00lsp  19746  ocv0  20366  ofco2  21056  tgidm  21585  pptbas  21613  tgrest  21764  iscnp2  21844  ist1-3  21954  discmp  22003  1stcfb  22050  lly1stc  22101  disllycmp  22103  dis1stc  22104  comppfsc  22137  txbas  22172  ptbasfi  22186  ptpjopn  22217  dfac14  22223  ptrescn  22244  xkoptsub  22259  fclsval  22613  ptcmplem2  22658  ptcmplem3  22659  cnextrel  22668  tsmsfbas  22733  ustuqtop  22852  prdsxmetlem  22975  ressprdsds  22978  prdsxmslem2  23136  zcld  23418  xrge0tsms  23439  metdsf  23453  metdsge  23454  minveclem1  24028  minveclem3b  24032  minveclem6  24038  uniioombllem4  24190  uniioombllem6  24192  ismbf3d  24258  i1f1lem  24293  reldv  24473  ellimc2  24480  limcflf  24484  limciun  24497  dvfval  24500  dvrec  24558  dvlipcn  24597  mdegle0  24678  ply1nzb  24723  quotlem  24896  taylfval  24954  ulmdvlem1  24995  ulmdvlem2  24996  ulmdvlem3  24997  psercn  25021  sqff1o  25767  lgsquadlem2  25965  disjxwwlksn  27690  wwlksnfi  27692  disjxwwlkn  27699  numclwwlk3lem2  28169  grpoidval  28296  grpoidinv2  28298  grpoinv  28308  minvecolem1  28657  minvecolem5  28664  minvecolem6  28665  adjbdln  29866  dfcnv2  30439  intimafv  30470  rexdiv  30628  gsumpart  30740  xrge0tsmsd  30742  fedgmullem2  31114  rspectopn  31220  zarcls  31227  zartopn  31228  esumnul  31417  esum0  31418  hasheuni  31454  esum2d  31462  ldgenpisyslem3  31534  measvuni  31583  measdivcstALTV  31594  ddemeas  31605  carsgclctunlem2  31687  eulerpartlemgs2  31748  probfinmeasbALTV  31797  0rrv  31819  signsplypnf  31930  signsply0  31931  hgt750lemb  32037  bnj226  32114  bnj98  32249  bnj517  32267  bnj893  32310  bnj1137  32377  subfacf  32535  subfacp1lem6  32545  cvmsss2  32634  cvmliftlem1  32645  nulssgt  33376  bj-rabtr  34372  relowlssretop  34780  fin2so  35044  matunitlindflem1  35053  ptrest  35056  poimirlem23  35080  poimirlem24  35081  poimirlem27  35084  poimirlem30  35087  poimirlem32  35089  cnambfre  35105  upixp  35167  0totbnd  35211  prdsbnd  35231  prdstotbnd  35232  cntotbnd  35234  rrnequiv  35273  ac6s6  35610  cdlemefrs32fva  37696  cdlemkid5  38231  cdlemk56  38267  dihf11lem  38562  addinvcom  39566  0dioph  39717  vdioph  39718  rmxyelqirr  39849  pw2f1ocnv  39976  pwinfi  40261  eliunov2  40378  fvmptiunrelexplb0d  40383  fvmptiunrelexplb1d  40385  iunrelexp0  40401  ntrrn  40823  dssmapntrcls  40829  mnurndlem1  40987  wessf1ornlem  41809  axccdom  41851  mpteq1df  41870  fsumiunss  42215  limcdm0  42258  liminfval2  42408  liminflelimsuplem  42415  cnrefiisplem  42469  0cnf  42517  dvsinax  42553  ioodvbdlimc1lem2  42572  ioodvbdlimc2lem  42574  dvnprodlem3  42588  iblempty  42605  fourierdlem89  42835  fourierdlem91  42837  fourierdlem100  42846  fourierdlem108  42854  fourierdlem112  42858  salexct3  42980  salgensscntex  42982  omeiunle  43154  0ome  43166  hoissrrn  43186  ovn0  43203  hoissrrn2  43215  hspmbl  43266  ovolval5lem2  43290  ovolval5lem3  43291  iunhoiioolem  43312  vonioolem2  43318  vonicclem2  43321  smflimlem1  43402  smfsuplem1  43440  smfinflem  43446  smflimsuplem1  43449  smflimsuplem2  43450  smflimsuplem3  43451  smflimsuplem4  43452  smflimsuplem5  43453  smflimsuplem7  43455  smfliminflem  43459  ralndv2  43660  iccelpart  43948  eliunxp2  44733  1arymaptf1  45054
  Copyright terms: Public domain W3C validator