Theorem rgen2 2616

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

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

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513

This theorem is referenced by:  rgen3  2617  invdisjrab  4077  f1stres  6305  f2ndres  6306  exmidonfinlem  7371  netap  7440  2onetap  7441  2omotaplemap  7443  mpomulf  8136  aptap  8797  divfnzn  9816  fnpfx  11209  wrd2ind  11255  1arith  12890  xpsff1o  13382  mgmidmo  13405  nmznsg  13750  isabli  13837  rhmfn  14136  cnsubmlem  14542  cnsubrglem  14544  txuni2  14930  divcnap  15239  abscncf  15259  recncf  15260  imcncf  15261  cjcncf  15262  reefiso  15451  ioocosf1o  15528  sgmf  15660  perfectlem2  15674  2lgslem1b  15768