Theorem rgen2 2630

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 2617	. 2 |- ( x e. A -> A. y e. B ph )
3	2	rgen 2597	1 |- A. x e. A A. y e. B ph

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2205   A.wral 2522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-4 1559  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2527

This theorem is referenced by:  rgen3  2631  invdisjrab  4109  f1stres  6368  f2ndres  6369  exmidonfinlem  7511  netap  7586  2onetap  7587  2omotaplemap  7589  mpomulf  8282  aptap  8944  zfidc  9678  divfnzn  9976  fnpfx  11399  wrd2ind  11445  1arith  13096  ballotfilem2  13178  xpsff1o  13619  mgmidmo  13641  nmznsg  13972  isabli  14059  rhmfn  14423  cnsubmlem  14858  cnsubrglem  14860  txuni2  15253  divcnap  15562  abscncf  15582  recncf  15583  imcncf  15584  cjcncf  15585  reefiso  15774  ioocosf1o  15851  sgmf  15986  perfectlem2  16000  2lgslem1b  16094