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 4510  dfom3 4622  rankval3 4673  rankuni2 4682  rankun 4683  scottex 4708  cplem1 4712  aceq5lem4 4730  kmlem1 4757  cardiun 4851  alephfplem4 4891  cflem 4897  cflecard 4904  cfeq0 4906  cfsuc 4907  dmrecpq 5066  1pr 5109  reclem2pr 5149  nnssre 5915  dfnn2 5924  nnind 5925  nnleltp1t 5942  xrsupsslem 6064  xrinfmsslem 6065  xrsup0 6085  dfuz 6190  seq1res 6313  ser1ref 6318  ser1f2 6320  seq1shftid 6342  icoshftf1oi 6395  uzinfm 6448  seq1seqz 6527  seq1seq0 6531  seqzresval 6545  seqzres 6546  seqzres2 6547  ser0f 6551  sqrlem6 6664  sqrlem13 6671  ref 6745  imf 6746  seq1bnd 6895  caure 6912  cauim 6913  ser1absdiflem 6914  bccl2t 6956  sumeq2 6970  ser1ser0 7033  serzref 7036  serz0 7038  serzmulc 7043  serzrelem 7046  climfnrcl 7096  climaddc 7117  climmulc 7118  clim2serz 7130  climserzle 7132  climabslem 7133  climabs 7134  climcj 7135  climre 7136  climim 7137  climcau 7141  caucvg3a 7149  caucvg3lem 7151  caucvg3t 7153  serzf0 7154  ser1f0 7155  iserzabslem 7163  cvgcmp2lem 7165  cvgcmp2clem 7167  cvgcmpub 7170  cvgcmp3c 7171  cvgcmp3cetlem1 7173  cvgcmp3cetlem2 7174  isummulc1 7197  isumcmpi 7200  isumsplit 7201  infcvglem2 7207  fnsmntlem 7210  fnsmnt 7211  geolimilem 7220  negfcncf 7254  ivthlem3 7268  ivthlem5 7270  ivthlem6 7271  ivthlem7 7272  ivthlem9 7274  isupivth 7275  dsupivthlem 7276  efcltlem1 7289  dfef2 7292  eff 7298  reefcl 7302  erelem2 7305  efaddlem3 7325  efaddlem5 7327  efaddlem6 7328  efaddlem16 7338  efaddlem18 7340  efaddlem19 7341  efaddlem26 7348  efaddlem27 7349  eff2 7355  ef1tllem 7366  ef01tllem1 7368  ef01tllem2 7369  ef01tllem2OLD 7370  eirrlem2 7375  eirrlem3 7376  eirrlem4 7377  eirrlem5 7378  efsep 7381  eflegeolem2 7399  sinf 7425  cosf 7426  infpn2 7494  ruclem33 7527  ruclem35 7529  isbasis3g 7598  indistop 7633  distop 7634  qdensere 7736  lmuni 7936  fsumcnlem 7974  iscms2i 7980  isgrpi 8027  grpidinv2 8045  grpinv 8054  isgrp2i 8061  cnid 8112  mulid 8117  cnring 8147  ringsn 8148  isvci 8186  isnvi 8217  va1cnlem 8330  ipasslem6 8480  ipasslem8 8482  ubthlem6 8519  minveclem10 8539  minveclem14 8543  minveclem39 8572  spwpr3OLD 8647  sinco 8652  cosco 8653  pilem2 8657  pilem3 8658  efif 8706  efifo 8714  effoi 8730  normlem6 8966  hilid 9013  hlim0 9090  hlimcaui 9091  shsspwh 9103  projlem8 9178  projlem13 9183  pjmf1 9646  df0op2 9663  dfiop2 9664  hoaddcom 9683  hoaddass 9687  hocadddir 9690  hocsubdir 9691  hoaddid1 9697  ho0co 9699  hoid1 9700  hoid1r 9701  honegsub 9707  hoddi 9899  lnopco0 9914  lnopunilem2 9921  elunop2t 9923  lnophmt 9929  cnlnadjlem8 9992  nmopadjlem 10007  nmoptri 10012  nmopco 10013  nmopcoadj 10019  pjnmop 10060  hmopidmpj 10065  pjsdi 10068  pjddi 10069  pjtot 10092  irredt 10307  cayleylem2 10395  idhme 10494  hmphre 10502  efilcp 10530  1ded 10614  0ded 10633  0cat 10634

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