Theorem rgen2w 3076

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

Syntax hints:  ∀wral 3063

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

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

This theorem is referenced by:  porpss  7558  fnmpoi  7883  relmpoopab  7905  cantnfvalf  9353  ixxf  13018  fzf  13172  fzof  13313  rexfiuz  14987  sadcf  16088  prdsvallem  17082  prdsds  17092  homfeq  17320  comfeq  17332  wunnat  17588  wunnatOLD  17589  eldmcoa  17696  catcfuccl  17750  catcfucclOLD  17751  relxpchom  17814  catcxpccl  17840  catcxpcclOLD  17841  plusffval  18247  grpsubfval  18538  lsmass  19190  efgval2  19245  dmdprd  19516  dprdval  19521  scaffval  20056  ipffval  20765  eltx  22627  xkotf  22644  txcnp  22679  txcnmpt  22683  txrest  22690  txlm  22707  txflf  23065  dscmet  23634  xrtgioo  23875  ishtpy  24041  opnmblALT  24672  tglnfn  26812  wwlksonvtx  28121  wspthnonp  28125  clwwlknondisj  28376  hlimreui  29502  aciunf1lem  30901  ofoprabco  30903  lsmssass  31492  dya2iocct  32147  icoreresf  35450  curfv  35684  ptrest  35703  poimirlem26  35730  rrnval  35912  atpsubN  37694  clsk3nimkb  41539  2arymaptf1  45887