Theorem rgen 1698

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

Syntax hints:   -> wi 3   e. wcel 958  A.wral 1645

This theorem is referenced by:  rgen2a 1699  mprg 1700  mprgbir 1701  rgen2 1723  r19.21be 1728  nrex 1729  reuss 2276  reuun1 2277  ral0 2358  unimax 2532  onssmin 3008  tfis 3127  finds 3156  finds2 3158  fnopab 3617  fopab 3827  fopabsn 3840  iunex 3863  canth 3907  elrnoprab 4125  nneneq 4512  dfom3 4630  rankval3 4681  rankuni2 4690  rankun 4691  scottex 4716  cplem1 4720  aceq5lem4 4738  kmlem1 4765  cardiun 4859  alephfplem4 4899  cflem 4905  cflecard 4912  cfeq0 4914  cfsuc 4915  dmrecpq 5074  1pr 5117  reclem2pr 5157  nnssre 5927  dfnn2 5936  nnind 5937  nnleltp1t 5954  xrsupsslem 6076  xrinfmsslem 6077  xrsup0 6097  dfuz 6202  seq1res 6327  ser1ref 6332  ser1f2 6334  seq1shftid 6356  icoshftf1oi 6409  uzinfm 6462  seq1seqz 6541  seq1seq0 6545  seqzresval 6559  seqzres 6560  seqzres2 6561  ser0f 6565  sqrlem6 6678  sqrlem13 6685  ref 6759  imf 6760  seq1bnd 6910  caure 6927  cauim 6928  ser1absdiflem 6929  bccl2t 6971  sumeq2 6985  ser1ser0 7048  serzref 7051  serz0 7053  serzmulc 7058  serzrelem 7061  climfnrcl 7111  climaddc 7132  climmulc 7133  clim2serz 7145  climserzle 7147  climabslem 7148  climabs 7149  climcj 7150  climre 7151  climim 7152  climcau 7156  caucvg3a 7164  caucvg3lem 7166  caucvg3t 7168  serzf0 7169  ser1f0 7170  iserzabslem 7178  cvgcmp2lem 7180  cvgcmp2clem 7182  cvgcmpub 7185  cvgcmp3c 7186  cvgcmp3cetlem1 7188  cvgcmp3cetlem2 7189  isummulc1 7212  isumcmpi 7215  isumsplit 7216  infcvglem2 7222  fnsmntlem 7225  fnsmnt 7226  geolimilem 7235  negfcncf 7269  ivthlem3 7283  ivthlem5 7285  ivthlem6 7286  ivthlem7 7287  ivthlem9 7289  isupivth 7290  dsupivthlem 7291  efcltlem1 7304  dfef2 7307  eff 7313  reefcl 7317  erelem2 7320  efaddlem3 7340  efaddlem5 7342  efaddlem6 7343  efaddlem16 7353  efaddlem18 7355  efaddlem19 7356  efaddlem26 7363  efaddlem27 7364  eff2 7370  ef1tllem 7381  ef01tllem1 7383  ef01tllem2 7384  ef01tllem2OLD 7385  eirrlem2 7390  eirrlem3 7391  eirrlem4 7392  eirrlem5 7393  efsep 7396  eflegeolem2 7414  sinf 7440  cosf 7441  infpn2 7509  ruclem33 7542  ruclem35 7544  isbasis3g 7613  indistop 7648  distop 7649  qdensere 7751  lmuni 7951  fsumcnlem 7989  iscms2i 7995  isgrpi 8042  grpidinv2 8060  grpinv 8069  isgrp2i 8076  cnid 8127  mulid 8132  cnring 8162  ringsn 8163  isvci 8201  isnvi 8232  va1cnlem 8345  ipasslem6 8495  ipasslem8 8497  ubthlem6 8534  minveclem10 8554  minveclem14 8558  minveclem39 8587  spwpr3OLD 8662  sinco 8667  cosco 8668  pilem2 8672  pilem3 8673  efif 8721  efifo 8729  effoi 8745  normlem6 8981  hilid 9028  hlim0 9105  hlimcaui 9106  shsspwh 9118  projlem8 9193  projlem13 9198  pjmf1 9661  df0op2 9678  dfiop2 9679  hoaddcom 9698  hoaddass 9702  hocadddir 9705  hocsubdir 9706  hoaddid1 9712  ho0co 9714  hoid1 9715  hoid1r 9716  honegsub 9722  hoddi 9914  lnopco0 9929  lnopunilem2 9936  elunop2t 9938  lnophmt 9944  cnlnadjlem8 10007  nmopadjlem 10022  nmoptri 10027  nmopco 10028  nmopcoadj 10034  pjnmop 10075  hmopidmpj 10080  pjsdi 10083  pjddi 10084  pjtot 10107  irredt 10322  cayleylem2 10410  idhme 10522  hmphre 10530  efilcp 10572  efilcpOLD 10573  1ded 10671  0ded 10690  0cat 10691

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

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

Copyright terms: Public domain