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  7663  fnmpoi  8005  mptmpoopabbrd  8015  relmpoopab  8027  cantnfvalf  9561  ixxf  13258  fzf  13414  fzof  13559  rexfiuz  15255  sadcf  16364  prdsvallem  17358  prdsds  17368  homfeq  17600  comfeq  17612  wunnat  17866  eldmcoa  17972  catcfuccl  18025  relxpchom  18087  catcxpccl  18113  plusffval  18520  grpsubfval  18862  lsmass  19548  efgval2  19603  dmdprd  19879  dprdval  19884  scaffval  20783  ipffval  21555  psdmul  22051  eltx  23453  xkotf  23470  txcnp  23505  txcnmpt  23509  txrest  23516  txlm  23533  txflf  23891  dscmet  24458  xrtgioo  24693  ishtpy  24869  opnmblALT  25502  zsoring  28301  tglnfn  28492  wwlksonvtx  29800  wspthnonp  29804  clwwlknondisj  30055  hlimreui  31183  aciunf1lem  32606  ofoprabco  32608  lsmssass  33340  dya2iocct  34254  icoreresf  37336  curfv  37590  ptrest  37609  poimirlem26  37636  rrnval  37817  atpsubN  39742  clsk3nimkb  44023  2arymaptf1  48648