Theorem rgen2w 3081

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

This proof depends on syntax axioms:  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827

This proof depends on definitions:  df-bi 210  df-ral 3077

This theorem is used by:  porpss  7743  fnmpoi  8081  mptmpoopabbrd  8094  relmpoopab  8105  curfv  8892  cantnfvalf  9666  ixxf  13486  fzf  13643  fzof  13790  rexfiuz  15515  sadcf  16623  prdsvallem  17625  prdsds  17635  homfeq  17868  comfeq  17880  wunnat  18134  eldmcoa  18240  catcfuccl  18293  relxpchom  18355  catcxpccl  18381  plusffval  18822  grpsubfval  19194  lsmass  19883  efgval2  19938  dmdprd  20214  dprdval  20219  scaffval  21155  ipffval  21954  psdmul  22487  eltx  23887  xkotf  23904  txcnp  23939  txcnmpt  23943  txrest  23950  txlm  23967  txflf  24325  dscmet  24891  xrtgioo  25126  ishtpy  25293  opnmblALT  25924  zsoring  28795  tglnfn  29010  tgplnfn  29253  wwlksonvtx  30444  wspthnonp  30448  clwwlknondisj  30702  hlimreui  31841  aciunf1lem  33256  ofoprabco  33258  lsmssass  33953  dya2iocct  34912  vonf1osev  35891  mh-inf3sn  37330  icoreresf  38276  ptrest  38538  poimirlem26  38565  rrnval  38762  disjimeceqbi  39739  atpsubN  40811  clsk3nimkb  45040  2arymaptf1  49765