Theorem rgen2 1723

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

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

This theorem is referenced by:  rgen3 1724  f1stres 4093  f2ndres 4094  foprab 4120  fnoprab2 4122  efcn 7423  nmcnilem 8337  sm1cnilem 8347  helch 9116  hsn0elch 9120  hhshsslem2 9138  shscl 9281  shintcl 9293  0cnop 9903  0cnfn 9904  idcnop 9905  lnophs 9926  nlelsh 9993  cnlnadjlem6 10005  hmopidmch 10079  fgsb 10570  fgsbOLD 10571  fgsb2 10580  1cat 10692

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975

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

Copyright terms: Public domain