Theorem rgen2w 3078

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

Syntax hints:  ∀wral 3065

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

This theorem depends on definitions:  df-bi 206  df-ral 3070

This theorem is referenced by:  porpss  7589  fnmpoi  7919  relmpoopab  7943  cantnfvalf  9432  ixxf  13098  fzf  13252  fzof  13393  rexfiuz  15068  sadcf  16169  prdsvallem  17174  prdsds  17184  homfeq  17412  comfeq  17424  wunnat  17681  wunnatOLD  17682  eldmcoa  17789  catcfuccl  17843  catcfucclOLD  17844  relxpchom  17907  catcxpccl  17933  catcxpcclOLD  17934  plusffval  18341  grpsubfval  18632  lsmass  19284  efgval2  19339  dmdprd  19610  dprdval  19615  scaffval  20150  ipffval  20862  eltx  22728  xkotf  22745  txcnp  22780  txcnmpt  22784  txrest  22791  txlm  22808  txflf  23166  dscmet  23737  xrtgioo  23978  ishtpy  24144  opnmblALT  24776  tglnfn  26917  wwlksonvtx  28229  wspthnonp  28233  clwwlknondisj  28484  hlimreui  29610  aciunf1lem  31008  ofoprabco  31010  lsmssass  31599  dya2iocct  32256  icoreresf  35532  curfv  35766  ptrest  35785  poimirlem26  35812  rrnval  35994  atpsubN  37774  clsk3nimkb  41657  2arymaptf1  46010