Theorem rgen 2159

Description: Generalization rule for restricted quantification.

Hypothesis

Ref	Expression
rgen.1	|- (x e. A -> ph)

Assertion

Ref	Expression
rgen	|- A.x e. A ph

Proof of Theorem rgen

Step	Hyp	Ref	Expression
1		df-ral 2109	. 2 |- (A.x e. A ph <-> A.x(x e. A -> ph))
2		rgen.1	. 2 |- (x e. A -> ph)
3	1, 2	mpgbir 1334	1 |- A.x e. A ph

Syntax hints:   -> wi 3   e. wcel 1300  A.wral 2105

This theorem is referenced by:  rgen2a 2160  rgen2aOLD 2161  mprg 2162  mprgbir 2163  rgen2 2186  r19.21be 2191  nrex 2192  r19.23ai 2209  reuss 2871  reuun1 2872  r19.2zb 2959  ral0 2974  unimax 3212  onssmin 3878  tfis 3938  omssnlim 3965  finds 3979  finds2 3981  fnopab 4548  fopab 4800  fopabsnOLD 4816  iunex 4839  elrnoprab 5067  canth 5112  nneneq 5606  dfom3 5737  rankval3 5792  rankuni2 5801  rankun 5802  scottex 5846  cplem1 5850  aceq5lem4 5900  kmlem1 5927  ficardom 5979  cardiun 6011  alephfplem4 6047  cflem 6053  cflecard 6060  cfeq0 6062  cfsuc 6063  dmrecpq 6226  1pr 6269  reclem2pr 6309  nnssre 7110  dfnn2 7119  nnind 7120  nnleltp1 7138  xrsupsslem 7285  xrinfmsslem 7286  xrsup0 7306  dfuzi 7414  zindd 7427  icoshftf1oii 7578  uzinfmi 7631  seq1res 7740  ser1refi 7745  ser1f2i 7747  seq1shftid 7769  seq1seqz 7784  seq1seq0 7788  seqzresval 7802  seqzres 7803  seqzres2 7804  ser0fi 7808  sqrlem6 7928  sqrlem13 7935  ref 8009  imf 8010  seq1bndi 8162  caurei 8179  cauimi 8180  ser1absdiflem 8181  bccl2 8223  sumeq2 8245  ser1ser0i 8308  serzrefi 8311  serz0 8313  serzmulci 8318  serzrelem 8321  climfnrcli 8371  climaddci 8392  climmulci 8393  clim2serzi 8405  climserzlei 8407  climabslem 8408  climabsi 8409  climcji 8410  climrei 8411  climimi 8412  climcaui 8416  caucvg3ai 8424  caucvg3lem 8426  caucvg3 8428  serzf0i 8429  iserzabslem 8438  cvgcmp2lem 8440  cvgcmp2clem 8442  cvgcmp2clemOLD 8443  cvgcmpubi 8446  cvgcmp3ci 8447  cvgcmp3cetlem1 8449  cvgcmp3cetlem2 8450  isummulc1 8473  isumcmpii 8476  isumspliti 8477  infcvglem2 8483  arisumilem 8486  arisumi 8487  explecnv 8495  geolimilem 8497  negfcncfi 8531  ivthlem3 8545  ivthlem5 8547  ivthlem6 8548  ivthlem7 8549  ivthlem9 8551  isupivthi 8552  dsupivthlem 8553  efcltlem1 8566  dfef2i 8569  eff 8575  reefcli 8579  erelem2 8582  efaddlem3 8602  efaddlem5 8604  efaddlem6 8605  efaddlem16 8615  efaddlem18 8617  efaddlem19 8618  efaddlem26 8625  efaddlem27 8626  eff2 8632  ef1tllem 8643  ef01tllem1 8645  ef01tllem2 8646  ef01tllem2OLD 8647  eirrlem2 8652  eirrlem3 8653  eirrlem4 8654  eirrlem5 8655  efsepi 8661  eflegeolem2 8679  sinf 8705  cosf 8706  infpn2 8778  ruclem33 8811  ruclem35 8813  isbasis3g 8882  distop 8919  qdensere 9027  lmuni 9229  fsumcnlem 9267  iscms2i 9273  isgrpi 9322  grpidinv2 9344  grpinv 9353  isgrp2i 9360  cnid 9435  mulid 9440  cnring 9489  ringsn 9490  isvci 9533  isnvi 9564  va1cnlem 9684  ipasslem6 9836  ipasslem8 9838  ubthlem6 9877  minveclem10 9899  minveclem14 9903  minveclem39 9932  spwpr4c 10009  sinco 10016  cosco 10017  pilem2 10021  pilem3 10022  efif 10075  efifo 10083  effoi 10099  normlem6 10614  hilid 10661  hlim0 10738  hlimcauii 10739  shsspwh 10751  projlem8 10826  projlem13 10831  pjmf1 11296  df0op2 11315  dfiop2 11316  hoaddcomi 11335  hoaddassi 11339  hocadddiri 11342  hocsubdiri 11343  hoaddid1i 11349  ho0coi 11351  hoid1i 11352  hoid1ri 11353  honegsubi 11359  hoddii 11551  lnopco0i 11566  lnopunilem2 11573  elunop2 11575  lnophm 11581  cnlnadjlem8 11644  nmopadjlem 11659  nmoptrii 11664  nmopcoi 11665  nmopcoadji 11671  pjnmopi 11719  hmopidmpji 11724  pjsdii 11727  pjddii 11728  pjtoi 11751  irred 11967  bnj890 12812  bnj580 13301  bnj1367 13511  bnj1497 13560  cayleylem2 13642  divalglem8 13703  gcdcllem1 13718  alginv 13743  algcvg 13744  algcvga 13747  algfx 13748  eucalgf 13751  isprm2lem 13774  3prm 13780  dfon2lem7 13855  epsetlike 13905  wfisg 13917  frinsg 13941  wfr3 13975  axbday 14012  axdense 14027  inpreima2 14468  cmpdom2 14482  cbicplem 14508  domrancur1b 14548  domncnt 14624  ranncnt 14625  prodeq2 14661  fincmpzer 14711  symgfo 14730  curgrpact 14735  fprodneg 14741  trooo 14758  trinv 14759  cexint2 14862  idhme 14879  hmphre 14884  usptoplem 14917  istopx 14918  prtoptop 14919  usptop 14920  efilcp 14922  idtrgrp 14978  trhom 14983  cntrsetlem 14999  1ded 15085  0ded 15104  0cat 15105  empistar 15219  trclval 15271  refref 15494  locfincomp 15514  ufilen 15579  opabex3 15701  upixp 15729  indexa 15753  fisup2g 15768  fsumltisumii 15822  fsumltisumi 15823  fsumleisumii 15825  fsumleisumi 15826  csbrni 15832  trirni 15833  mettrifi2 15848  cncfres 15895  sstotbnd 15936  bfplem7 16004  recms 16010  phtpycom 16050  phtpycolem3 16053  phtpycolem4 16054  pcocn 16076  pcohtpylem3 16082  lubid 16807  isatlati 17015  isgrpiNEW 17115  grpidinv2NEW 17119  grpinvNEW 17128  atpsub 17233

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305

This theorem depends on definitions:  df-bi 164  df-ral 2109

Copyright terms: Public domain