MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rgen2w Unicode version

Theorem rgen2w 2763
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
StepHypRef Expression
1 rgenw.1 . . 3
21rgenw 2762 . 2
32rgenw 2762 1
Colors of variables: wff setvar class
Syntax hints:  A.wral 2694
This theorem is referenced by:  porpss  6334  fnmpt2i  6612  relmpt2opab  6624  cantnfvalf  7820  ixxf  11255  fzf  11385  fzof  11491  rexfiuz  12776  sadcf  13589  prdsval  14333  prdsds  14342  homfeq  14573  comfeq  14585  wunnat  14806  eldmcoa  14873  catcfuccl  14917  relxpchom  14931  catcxpccl  14957  plusffval  15367  lsmass  16104  efgval2  16158  dmdprd  16368  dprdval  16370  scaffval  16779  ipffval  17785  eltx  18845  xkotf  18862  txcnp  18897  txcnmpt  18901  txrest  18908  txlm  18925  txflf  19283  dscmet  19865  xrtgioo  20083  ishtpy  20244  opnmblALT  20783  tglnfn  22718  hlimreui  24321  ofoprabco  25662  pstmxmet  26033  dya2iocct  26404  sseqfv2  26480  ptrest  28096  rrnval  28397  numclwwlkdisj  30347  atpsubN  32834
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586
This theorem depends on definitions:  df-bi 179  df-ral 2699
  Copyright terms: Public domain W3C validator