Theorem rgen2 2636

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

Hypothesis

Ref	Expression
rgen2.1	|- ( ( x e. A /\ y e. B ) -> ph )

Assertion

Ref	Expression
rgen2	|- A. x e. A A. y e. B ph

Distinct variable groups:   x, y   y, A

Allowed substitution hints:   ph( x, y)   A( x)   B( x, y)

Proof of Theorem rgen2

Step	Hyp	Ref	Expression
1		rgen2.1	. . 3 |- ( ( x e. A /\ y e. B ) -> ph )
2	1	ralrimiva 2623	. 2 |- ( x e. A -> A. y e. B ph )
3	2	rgen 2603	1 |- A. x e. A A. y e. B ph

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   e. wcel 2209   A.wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is used by:  rgen3  2637  invdisjrab  4124  f1stres  6397  f2ndres  6398  exmidonfinlem  7551  netap  7626  2onetap  7627  2omotaplemap  7629  mpomulf  8322  aptap  8986  zfidc  9734  divfnzn  10037  fnpfx  11471  wrd2ind  11517  1arith  13175  ballotfilem2  13286  xpsff1o  13729  mgmidmo  13751  nmznsg  14075  isabli  14193  rhmfn  14588  cnsubmlem  15024  cnsubrglem  15026  txuni2  15482  divcnap  15791  abscncf  15811  recncf  15812  imcncf  15813  cjcncf  15814  reefiso  16003  ioocosf1o  16082  sgmf  16255  perfectlem2  16300  2lgslem1b  16413