Theorem rgen2w 3085

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

This proof depends on syntax axioms:  ∀wral 3080

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

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

This theorem is used by:  porpss  7764  fnmpoi  8103  mptmpoopabbrd  8116  relmpoopab  8128  curfv  8917  cantnfvalf  9690  ixxf  13510  fzf  13667  fzof  13814  rexfiuz  15541  sadcf  16649  prdsvallem  17651  prdsds  17661  homfeq  17894  comfeq  17906  wunnat  18160  eldmcoa  18266  catcfuccl  18319  relxpchom  18381  catcxpccl  18407  plusffval  18848  grpsubfval  19220  lsmass  19910  efgval2  19965  dmdprd  20241  dprdval  20246  scaffval  21182  ipffval  21981  psdmul  22514  eltx  23914  xkotf  23931  txcnp  23966  txcnmpt  23970  txrest  23977  txlm  23994  txflf  24352  dscmet  24918  xrtgioo  25153  ishtpy  25320  opnmblALT  25951  zsoring  28822  tglnfn  29037  tgplnfn  29280  wwlksonvtx  30471  wspthnonp  30475  clwwlknondisj  30729  hlimreui  31868  aciunf1lem  33325  ofoprabco  33327  lsmssass  34020  dya2iocct  34979  vonf1osev  36039  vsmext  36088  mh-inf3sn  37507  icoreresf  38466  ptrest  38728  poimirlem26  38755  rrnval  38952  disjimeceqbi  39929  atpsubN  41001  clsk3nimkb  45230  2arymaptf1  49968  parhomssun  50950