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  6311  f2ndres  6312  exmidonfinlem  7382  netap  7451  2onetap  7452  2omotaplemap  7454  mpomulf  8147  aptap  8808  divfnzn  9828  fnpfx  11225  wrd2ind  11271  1arith  12906  xpsff1o  13398  mgmidmo  13421  nmznsg  13766  isabli  13853  rhmfn  14152  cnsubmlem  14558  cnsubrglem  14560  txuni2  14946  divcnap  15255  abscncf  15275  recncf  15276  imcncf  15277  cjcncf  15278  reefiso  15467  ioocosf1o  15544  sgmf  15676  perfectlem2  15690  2lgslem1b  15784