Theorem rgen2w 3049

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 3048	. 2 ⊢ ∀𝑦 ∈ 𝐵 𝜑
3	2	rgenw 3048	1 ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑

Syntax hints:  ∀wral 3044

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

This theorem depends on definitions:  df-bi 207  df-ral 3045

This theorem is referenced by:  porpss  7683  fnmpoi  8028  mptmpoopabbrd  8038  relmpoopab  8050  cantnfvalf  9594  ixxf  13292  fzf  13448  fzof  13593  rexfiuz  15290  sadcf  16399  prdsvallem  17393  prdsds  17403  homfeq  17635  comfeq  17647  wunnat  17901  eldmcoa  18007  catcfuccl  18060  relxpchom  18122  catcxpccl  18148  plusffval  18555  grpsubfval  18897  lsmass  19583  efgval2  19638  dmdprd  19914  dprdval  19919  scaffval  20818  ipffval  21590  psdmul  22086  eltx  23488  xkotf  23505  txcnp  23540  txcnmpt  23544  txrest  23551  txlm  23568  txflf  23926  dscmet  24493  xrtgioo  24728  ishtpy  24904  opnmblALT  25537  zsoring  28336  tglnfn  28527  wwlksonvtx  29835  wspthnonp  29839  clwwlknondisj  30090  hlimreui  31218  aciunf1lem  32636  ofoprabco  32638  lsmssass  33366  dya2iocct  34264  icoreresf  37333  curfv  37587  ptrest  37606  poimirlem26  37633  rrnval  37814  atpsubN  39740  clsk3nimkb  44022  2arymaptf1  48635