Theorem rgen2w 3054

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

Syntax hints:  ∀wral 3049

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

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

This theorem is referenced by:  porpss  7670  fnmpoi  8012  mptmpoopabbrd  8022  relmpoopab  8034  cantnfvalf  9572  ixxf  13269  fzf  13425  fzof  13570  rexfiuz  15269  sadcf  16378  prdsvallem  17372  prdsds  17382  homfeq  17615  comfeq  17627  wunnat  17881  eldmcoa  17987  catcfuccl  18040  relxpchom  18102  catcxpccl  18128  plusffval  18569  grpsubfval  18911  lsmass  19596  efgval2  19651  dmdprd  19927  dprdval  19932  scaffval  20829  ipffval  21601  psdmul  22107  eltx  23510  xkotf  23527  txcnp  23562  txcnmpt  23566  txrest  23573  txlm  23590  txflf  23948  dscmet  24514  xrtgioo  24749  ishtpy  24925  opnmblALT  25558  zsoring  28367  tglnfn  28568  wwlksonvtx  29877  wspthnonp  29881  clwwlknondisj  30135  hlimreui  31263  aciunf1lem  32689  ofoprabco  32691  lsmssass  33432  dya2iocct  34386  icoreresf  37496  curfv  37740  ptrest  37759  poimirlem26  37786  rrnval  37967  atpsubN  39952  clsk3nimkb  44223  2arymaptf1  48841