Theorem rgen2 2580

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

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

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2477

This theorem is referenced by:  rgen3  2581  f1stres  6203  f2ndres  6204  exmidonfinlem  7243  netap  7304  2onetap  7305  2omotaplemap  7307  mpomulf  7999  aptap  8659  divfnzn  9676  1arith  12495  xpsff1o  12922  mgmidmo  12945  nmznsg  13272  isabli  13359  rhmfn  13652  cnsubmlem  14048  cnsubrglem  14050  txuni2  14401  divcnap  14700  abscncf  14717  recncf  14718  imcncf  14719  cjcncf  14720  reefiso  14860  ioocosf1o  14937