Theorem rgen2 2575

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

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

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 1457  ax-gen 1459  ax-4 1520  ax-17 1536

This theorem depends on definitions:  df-bi 117  df-nf 1471  df-ral 2472

This theorem is referenced by:  rgen3  2576  f1stres  6177  f2ndres  6178  exmidonfinlem  7209  netap  7270  2onetap  7271  2omotaplemap  7273  aptap  8624  divfnzn  9638  1arith  12382  xpsff1o  12790  mgmidmo  12813  nmznsg  13117  isabli  13199  rhmfn  13482  cnsubmlem  13841  cnsubrglem  13843  txuni2  14139  divcnap  14438  abscncf  14455  recncf  14456  imcncf  14457  cjcncf  14458  reefiso  14581  ioocosf1o  14658