Theorem rgen2w 3077

Description: Generalization rule for restricted quantification. Note that 𝑥 and 𝑦 needn't be distinct. (Contributed by NM, 18-Jun-2014.)

Hypothesis

Ref	Expression
rgenw.1	⊢ 𝜑

Assertion

Ref	Expression
rgen2w	⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑

Proof of Theorem rgen2w

Step	Hyp	Ref	Expression
1		rgenw.1	. . 3 ⊢ 𝜑
2	1	rgenw 3076	. 2 ⊢ ∀𝑦 ∈ 𝐵 𝜑
3	2	rgenw 3076	1 ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑

Syntax hints:  ∀wral 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873

This theorem depends on definitions:  df-bi 198  df-ral 3069

This theorem is referenced by:  porpss  7109  fnmpt2i  7410  relmpt2opab  7431  cantnfvalf  8747  ixxf  12409  fzf  12559  fzof  12697  rexfiuz  14317  sadcf  15404  prdsval  16343  prdsds  16352  homfeq  16581  comfeq  16593  wunnat  16843  eldmcoa  16942  catcfuccl  16986  relxpchom  17049  catcxpccl  17075  plusffval  17475  lsmass  18310  efgval2  18364  dmdprd  18625  dprdval  18630  scaffval  19111  ipffval  20230  eltx  21612  xkotf  21629  txcnp  21664  txcnmpt  21668  txrest  21675  txlm  21692  txflf  22050  dscmet  22617  xrtgioo  22849  ishtpy  23011  opnmblALT  23611  tglnfn  25684  wwlksonvtx  27006  wspthnonp  27014  clwwlknondisj  27308  clwwlknondisjOLD  27313  hlimreui  28453  aciunf1lem  29819  ofoprabco  29821  dya2iocct  30699  icoreresf  33554  curfv  33739  ptrest  33758  poimirlem26  33785  rrnval  33974  atpsubN  35577  clsk3nimkb  38878