Theorem rgen2 2563

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

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

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460

This theorem is referenced by:  rgen3  2564  f1stres  6162  f2ndres  6163  exmidonfinlem  7194  netap  7255  2onetap  7256  2omotaplemap  7258  aptap  8609  divfnzn  9623  1arith  12367  xpsff1o  12773  mgmidmo  12796  nmznsg  13078  isabli  13108  cnsubmlem  13511  cnsubrglem  13513  txuni2  13795  divcnap  14094  abscncf  14111  recncf  14112  imcncf  14113  cjcncf  14114  reefiso  14237  ioocosf1o  14314