Theorem rgen2w 3056

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

Syntax hints:  ∀wral 3051

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 3052

This theorem is referenced by:  porpss  7721  fnmpoi  8069  mptmpoopabbrd  8079  relmpoopab  8093  cantnfvalf  9679  ixxf  13372  fzf  13528  fzof  13673  rexfiuz  15366  sadcf  16472  prdsvallem  17468  prdsds  17478  homfeq  17706  comfeq  17718  wunnat  17972  eldmcoa  18078  catcfuccl  18131  relxpchom  18193  catcxpccl  18219  plusffval  18624  grpsubfval  18966  lsmass  19650  efgval2  19705  dmdprd  19981  dprdval  19986  scaffval  20837  ipffval  21608  psdmul  22104  eltx  23506  xkotf  23523  txcnp  23558  txcnmpt  23562  txrest  23569  txlm  23586  txflf  23944  dscmet  24511  xrtgioo  24746  ishtpy  24922  opnmblALT  25556  tglnfn  28526  wwlksonvtx  29837  wspthnonp  29841  clwwlknondisj  30092  hlimreui  31220  aciunf1lem  32640  ofoprabco  32642  lsmssass  33417  dya2iocct  34312  icoreresf  37370  curfv  37624  ptrest  37643  poimirlem26  37670  rrnval  37851  atpsubN  39772  clsk3nimkb  44064  2arymaptf1  48633