Theorem rgen2w 3072

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

Syntax hints:  ∀wral 3067

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

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

This theorem is referenced by:  porpss  7762  fnmpoi  8111  mptmpoopabbrd  8121  relmpoopab  8135  cantnfvalf  9734  ixxf  13417  fzf  13571  fzof  13713  rexfiuz  15396  sadcf  16499  prdsvallem  17514  prdsds  17524  homfeq  17752  comfeq  17764  wunnat  18024  wunnatOLD  18025  eldmcoa  18132  catcfuccl  18186  catcfucclOLD  18187  relxpchom  18250  catcxpccl  18276  catcxpcclOLD  18277  plusffval  18684  grpsubfval  19023  lsmass  19711  efgval2  19766  dmdprd  20042  dprdval  20047  scaffval  20900  ipffval  21689  psdmul  22193  eltx  23597  xkotf  23614  txcnp  23649  txcnmpt  23653  txrest  23660  txlm  23677  txflf  24035  dscmet  24606  xrtgioo  24847  ishtpy  25023  opnmblALT  25657  tglnfn  28573  wwlksonvtx  29888  wspthnonp  29892  clwwlknondisj  30143  hlimreui  31271  aciunf1lem  32680  ofoprabco  32682  lsmssass  33395  dya2iocct  34245  icoreresf  37318  curfv  37560  ptrest  37579  poimirlem26  37606  rrnval  37787  atpsubN  39710  clsk3nimkb  44002  2arymaptf1  48387