Theorem rgen2 1715

Description: Generalization rule for restricted quantification.

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

Proof of Theorem rgen2

Step	Hyp	Ref	Expression
1		rgen2.1	. . 3 |- ((x e. A /\ y e. B) -> ph)
2	1	r19.21aiva 1706	. 2 |- (x e. A -> A.y e. B ph)
3	2	rgen 1690	1 |- A.x e. A A.y e. B ph

Syntax hints:   -> wi 3   /\ wa 223   e. wcel 955  A.wral 1637

This theorem is referenced by:  rgen3 1716  f1stres 4077  f2ndres 4078  foprab 4104  fnoprab2 4106  efcn 7363  nmcnilem 8272  sm1cnilem 8281  helch 9037  hsn0elch 9041  hhshsslem2 9058  shscl 9196  shintcl 9208  0cnop 9819  0cnfn 9820  idcnop 9821  lnophs 9841  nlelsh 9908  cnlnadjlem6 9920  hmopidmch 9990  fgsb 10444  fgsb2 10449  1cat 10536

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972

This theorem depends on definitions:  df-bi 147  df-an 225  df-ral 1641

Copyright terms: Public domain