Theorem rgen 1744

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

Syntax hints:   -> wi 3   e. wcel 994  A.wral 1691

This theorem is referenced by:  rgen2a 1745  mprg 1746  mprgbir 1747  rgen2 1769  r19.21be 1774  nrex 1775  reuss 2328  reuun1 2329  ral0 2412  unimax 2599  onssmin 3154  tfis 3208  finds 3244  finds2 3246  fnopab 3724  fopab 3941  fopabsn 3954  iunex 3977  elrnoprab 4187  canth 4205  nneneq 4659  dfom3 4776  rankval3 4827  rankuni2 4836  rankun 4837  scottex 4862  cplem1 4866  aceq5lem4 4884  kmlem1 4911  ficardom 4977  cardiun 5009  alephfplem4 5049  cflem 5055  cflecard 5062  cfeq0 5064  cfsuc 5065  dmrecpq 5228  1pr 5271  reclem2pr 5311  nnssre 6072  dfnn2 6081  nnind 6082  nnleltp1 6100  xrsupsslem 6244  xrinfmsslem 6245  xrsup0 6265  dfuzi 6373  zindd 6386  icoshftf1oii 6536  uzinfmi 6589  seq1res 6692  ser1refi 6697  ser1f2i 6699  seq1shftid 6721  seq1seqz 6736  seq1seq0 6740  seqzresval 6754  seqzres 6755  seqzres2 6756  ser0fi 6760  sqrlem6 6879  sqrlem13 6886  ref 6960  imf 6961  seq1bndi 7113  caurei 7130  cauimi 7131  ser1absdiflem 7132  bccl2 7174  sumeq2 7188  ser1ser0i 7251  serzrefi 7254  serz0 7256  serzmulci 7261  serzrelem 7264  climfnrcli 7314  climaddci 7335  climmulci 7336  clim2serzi 7348  climserzlei 7350  climabslem 7351  climabsi 7352  climcji 7353  climrei 7354  climimi 7355  climcaui 7359  caucvg3ai 7367  caucvg3lem 7369  caucvg3 7371  serzf0i 7372  iserzabslem 7381  cvgcmp2lem 7383  cvgcmp2clem 7385  cvgcmp2clemOLD 7386  cvgcmpubi 7389  cvgcmp3ci 7390  cvgcmp3cetlem1 7392  cvgcmp3cetlem2 7393  isummulc1 7416  isumcmpii 7419  isumspliti 7420  infcvglem2 7426  arisumilem 7429  arisumi 7430  explecnv 7438  geolimilem 7440  negfcncfi 7474  ivthlem3 7488  ivthlem5 7490  ivthlem6 7491  ivthlem7 7492  ivthlem9 7494  isupivthi 7495  dsupivthlem 7496  efcltlem1 7509  dfef2i 7512  eff 7518  reefcli 7522  erelem2 7525  efaddlem3 7545  efaddlem5 7547  efaddlem6 7548  efaddlem16 7558  efaddlem18 7560  efaddlem19 7561  efaddlem26 7568  efaddlem27 7569  eff2 7575  ef1tllem 7586  ef01tllem1 7588  ef01tllem2 7589  ef01tllem2OLD 7590  eirrlem2 7595  eirrlem3 7596  eirrlem4 7597  eirrlem5 7598  efsepi 7604  eflegeolem2 7622  sinf 7648  cosf 7649  infpn2 7721  ruclem33 7754  ruclem35 7756  isbasis3g 7825  distop 7861  qdensere 7961  lmuni 8162  fsumcnlem 8200  iscms2i 8206  isgrpi 8255  grpidinv2 8277  grpinv 8286  isgrp2i 8293  cnid 8368  mulid 8373  cnring 8404  ringsn 8405  isvci 8448  isnvi 8479  va1cnlem 8599  ipasslem6 8751  ipasslem8 8753  ubthlem6 8792  minveclem10 8814  minveclem14 8818  minveclem39 8847  spwpr4c 8928  sinco 8934  cosco 8935  pilem2 8939  pilem3 8940  efif 8993  efifo 9001  effoi 9017  normlem6 9257  hilid 9304  hlim0 9381  hlimcauii 9382  shsspwh 9394  projlem8 9469  projlem13 9474  pjmf1 9939  df0op2 9958  dfiop2 9959  hoaddcomi 9978  hoaddassi 9982  hocadddiri 9985  hocsubdiri 9986  hoaddid1i 9992  ho0coi 9994  hoid1i 9995  hoid1ri 9996  honegsubi 10002  hoddii 10193  lnopco0i 10208  lnopunilem2 10215  elunop2 10217  lnophm 10223  cnlnadjlem8 10286  nmopadjlem 10301  nmoptrii 10306  nmopcoi 10307  nmopcoadji 10313  pjnmopi 10355  hmopidmpji 10360  pjsdii 10363  pjddii 10364  pjtoi 10387  irred 10604  cayleylem2 10695  domncnt 10872  ranncnt 10873  idhme 11028  hmphre 11036  efilcp 11083  1ded 11192  0ded 11211  0cat 11212  r19.2zb 11393  refref 11555  locfincomp 11575  ufilen 11664  opabex3 11806  upixp 11823  indexa 11845  fsumltisumii 11885  fsumltisumi 11886  fsumleisumii 11888  fsumleisumi 11889  csbrni 11895  trirni 11896  mettrifi2 11913  cncfres 11956  sstotbnd 11992  bfplem7 12060  recms 12066  phtpycom 12092  phtpycolem3 12095  phtpycolem4 12096

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

This theorem depends on definitions:  df-bi 145  df-ral 1695

Copyright terms: Public domain