Theorem rgen2 2592

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

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

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489

This theorem is referenced by:  rgen3  2593  f1stres  6245  f2ndres  6246  exmidonfinlem  7301  netap  7366  2onetap  7367  2omotaplemap  7369  mpomulf  8062  aptap  8723  divfnzn  9742  1arith  12690  xpsff1o  13181  mgmidmo  13204  nmznsg  13549  isabli  13636  rhmfn  13934  cnsubmlem  14340  cnsubrglem  14342  txuni2  14728  divcnap  15037  abscncf  15057  recncf  15058  imcncf  15059  cjcncf  15060  reefiso  15249  ioocosf1o  15326  sgmf  15458  perfectlem2  15472  2lgslem1b  15566