Theorem rgen2 2882

Description: Generalization rule for restricted quantification, with two quantifiers. (Contributed by NM, 30-May-1999.)

Hypothesis

Ref	Expression
rgen2.1

Assertion

Ref	Expression
rgen2

Distinct variable groups:   ,   ,

Proof of Theorem rgen2

Step	Hyp	Ref	Expression
1		rgen2.1	. . 3
2	1	ralrimiva 2871	. 2
3	2	rgen 2817	1

Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818  A.wral 2807

This theorem is referenced by:  rgen3  2883  f1stres  6822  f2ndres  6823  smobeth  8982  disjxwrd  12680  wrd2ind  12703  smupf  14128  xpsff1o  14965  efgmf  16731  efglem  16734  txuni2  20066  divcn  21372  abscncf  21405  recncf  21406  imcncf  21407  cjcncf  21408  cnllycmp  21456  bndth  21458  dyadf  22000  cxpcn3  23122  sgmf  23419  smcnlem  25607  helch  26161  hsn0elch  26166  hhshsslem2  26184  shscli  26235  shintcli  26247  0cnop  26898  0cnfn  26899  idcnop  26900  lnophsi  26920  nlelshi  26979  cnlnadjlem6  26991  cnzh  27951  rezh  27952  cnllyscon  28690  rellyscon  28696  mblfinlem1  30051  mblfinlem2  30052  fneref  30168  frmx  30849  frmy  30850  2zrngnmrid  32756  ldepslinc  33110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704

This theorem depends on definitions:  df-bi 185  df-an 371  df-ral 2812