Theorem rgen2w 3083

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

Syntax hints:  ∀wral 3078

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

This theorem depends on definitions:  df-bi 209  df-ral 3079

This theorem is referenced by:  porpss  7712  fnmpoi  8053  mptmpoopabbrd  8064  relmpoopab  8075  cantnfvalf  9622  ixxf  13361  fzf  13518  fzof  13663  rexfiuz  15377  sadcf  16489  prdsvallem  17485  prdsds  17495  homfeq  17728  comfeq  17740  wunnat  17994  eldmcoa  18100  catcfuccl  18153  relxpchom  18215  catcxpccl  18241  plusffval  18682  grpsubfval  19027  lsmass  19711  efgval2  19766  dmdprd  20042  dprdval  20047  scaffval  20949  ipffval  21702  psdmul  22233  eltx  23630  xkotf  23647  txcnp  23682  txcnmpt  23686  txrest  23693  txlm  23710  txflf  24068  dscmet  24634  xrtgioo  24869  ishtpy  25036  opnmblALT  25667  zsoring  28504  tglnfn  28718  tgplnfn  28984  wwlksonvtx  30057  wspthnonp  30061  clwwlknondisj  30315  hlimreui  31444  aciunf1lem  32866  ofoprabco  32868  lsmssass  33590  dya2iocct  34579  vonf1osev  35459  mh-inf3sn  36907  icoreresf  37851  curfv  38104  ptrest  38123  poimirlem26  38150  rrnval  38331  disjimeceqbi  39310  atpsubN  40382  clsk3nimkb  44621  2arymaptf1  49280