Theorem rgen2 1770

Description: Generalization rule for restricted quantification.

Hypothesis

Ref	Expression
rgen2.1	⊢ ((x ∈ A ⋀ y ∈ B) → φ)

Assertion

Ref	Expression
rgen2	⊢ ∀x ∈ A ∀y ∈ B φ

Distinct variable groups:   x,y   y,A

Proof of Theorem rgen2

Step	Hyp	Ref	Expression
1		rgen2.1	. . 3 ⊢ ((x ∈ A ⋀ y ∈ B) → φ)
2	1	r19.21aiva 1761	. 2 ⊢ (x ∈ A → ∀y ∈ B φ)
3	2	rgen 1745	1 ⊢ ∀x ∈ A ∀y ∈ B φ

Syntax hints:   → wi 3   ⋀ wa 230   ∈ wcel 999  ∀wral 1692

This theorem is referenced by:  rgen3 1771  f1stres 4151  f2ndres 4152  foprab 4178  fnoprab2 4180  efcn 7514  nmcnilem 8421  sm1cnilem 8431  helch 9199  hsn0elch 9203  hhshsslem2 9221  shscli 9364  shintcli 9376  0cnop 9986  0cnfn 9987  idcnop 9988  lnophsi 10009  nlelshi 10076  cnlnadjlem6 10088  hmopidmchi 10162  fgsb 10663  fgsb2 10668  1cat 10774

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1004  ax-17 1012  ax-4 1014  ax-5o 1016

This theorem depends on definitions:  df-bi 154  df-an 232  df-ral 1696

Copyright terms: Public domain