Theorem rgen 1695

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 1646	. 2 |- (A.x e. A ph <-> A.x(x e. A -> ph))
2		rgen.1	. 2 |- (x e. A -> ph)
3	1, 2	mpgbir 986	1 |- A.x e. A ph

Syntax hints:   -> wi 3   e. wcel 956  A.wral 1642

This theorem is referenced by:  rgen2a 1696  mprg 1697  mprgbir 1698  rgen2 1720  r19.21be 1725  nrex 1726  reuss 2272  reuun1 2273  ral0 2354  unimax 2527  onssmin 3003  tfis 3122  finds 3151  finds2 3153  fnopab 3609  fopab 3818  fopabsn 3831  iunex 3854  canth 3898  elrnoprab 4115  nneneq 4498  dfom3 4610  rankval3 4661  rankuni2 4670  rankun 4671  scottex 4696  cplem1 4700  aceq5lem4 4718  kmlem1 4745  cardiun 4839  alephfplem4 4879  cflem 4885  cflecard 4892  cfeq0 4894  cfsuc 4895  dmrecpq 5054  1pr 5097  reclem2pr 5137  nnssre 5883  dfnn2 5892  nnind 5893  nnleltp1t 5909  xrsupsslem 6031  xrinfmsslem 6032  xrsup0 6052  dfuz 6158  seq1res 6272  ser1ref 6277  ser1f2 6279  seq1shftid 6301  icoshftf1oi 6350  uzinfm 6402  seq1seqz 6481  seq1seq0 6485  seqzresval 6499  seqzres 6500  seqzres2 6501  ser0f 6505  sqrlem6 6616  sqrlem13 6623  ref 6698  imf 6699  seq1bnd 6855  caure 6872  cauim 6873  ser1absdiflem 6874  bccl2t 6917  sumeq2 6931  ser1ser0 6994  serzref 6997  serz0 6999  serzmulc 7004  serzrelem 7007  climfnrcl 7056  climaddc 7076  climmulc 7077  clim2serz 7089  climserzle 7091  climabslem 7092  climabs 7093  climcj 7094  climre 7095  climim 7096  climcau 7100  caucvg3a 7108  caucvg3lem 7110  caucvg3t 7112  serzf0 7113  ser1f0 7114  iserzabslem 7122  cvgcmp2lem 7124  cvgcmp2clem 7126  cvgcmpub 7129  cvgcmp3c 7130  cvgcmp3cetlem1 7132  cvgcmp3cetlem2 7133  isummulc1 7155  isumcmpi 7158  isumsplit 7159  infcvglem2 7165  fnsmntlem 7168  fnsmnt 7169  geolimilem 7178  negfcncf 7212  ivthlem3 7226  ivthlem5 7228  ivthlem6 7229  ivthlem7 7230  ivthlem9 7232  isupivth 7233  dsupivthlem 7234  ivthlem4OLD 7236  ivthlem5OLD 7237  ivthlem6OLD 7238  ivthlem7OLD 7239  efcltlem1 7254  dfef2 7257  eff 7263  reefcl 7267  erelem2 7270  efaddlem3 7290  efaddlem5 7292  efaddlem6 7293  efaddlem16 7303  efaddlem18 7305  efaddlem19 7306  efaddlem26 7313  efaddlem27 7314  eff2 7320  ef1tllem 7331  ef01tllem1 7333  ef01tllem2 7334  eirrlem2 7339  eirrlem3 7340  eirrlem4 7341  eirrlem5 7342  efsep 7345  eflegeolem2 7362  reeff1olem1OLD 7374  sinf 7390  cosf 7391  infpn2 7460  ruclem33 7493  ruclem35 7495  isbasis3g 7563  indistop 7598  distop 7599  qdensere 7701  lmuni 7902  fsumcnlem 7939  iscms2i 7945  isgrpi 7992  grpidinv2 8010  grpinv 8019  isgrp2i 8026  cnid 8079  mulid 8084  cnring 8114  ringsn 8115  isvci 8153  isnvi 8184  va1cnlem 8292  ipasslem6 8439  ipasslem8 8441  ubthlem6 8478  minveclem10 8498  minveclem14 8502  minveclem39 8531  sinco 8605  cosco 8606  pilem2 8610  pilem3 8611  efif 8655  efifo 8663  effoi 8684  normlem6 8920  hilid 8967  hlim0 9044  hlimcaui 9045  shsspwh 9057  projlem8 9132  projlem13 9137  pjmf1 9601  df0op2 9618  dfiop2 9619  hoaddcom 9638  hoaddass 9642  hocadddir 9645  hocsubdir 9646  hoaddid1 9652  ho0co 9654  hoid1 9655  hoid1r 9656  honegsub 9662  hoddi 9852  lnopco0 9867  lnopunilem2 9874  elunop2t 9876  lnophmt 9882  cnlnadjlem8 9945  nmopadjlem 9960  nmoptri 9965  nmopco 9966  nmopcoadj 9972  pjnmop 10013  hmopidmpj 10018  pjsdi 10021  pjddi 10022  pjtot 10045  irredt 10259  cayleylem2 10344  idhme 10445  hmphre 10453  efilcp 10481  1ded 10551  0ded 10570  0cat 10571

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

This theorem depends on definitions:  df-bi 147  df-ral 1646

Copyright terms: Public domain