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

Theorem rgen2w 2819
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 2818 . 2
32rgenw 2818 1
Colors of variables: wff setvar class
Syntax hints:  A.wral 2807
This theorem is referenced by:  porpss  6584  fnmpt2i  6869  relmpt2opab  6882  cantnfvalf  8105  ixxf  11568  fzf  11705  fzof  11826  rexfiuz  13180  sadcf  14103  prdsval  14852  prdsds  14861  homfeq  15089  comfeq  15101  wunnat  15325  eldmcoa  15392  catcfuccl  15436  relxpchom  15450  catcxpccl  15476  plusffval  15877  lsmass  16688  efgval2  16742  dmdprd  17029  dprdval  17034  dprdvalOLD  17036  scaffval  17530  ipffval  18683  eltx  20069  xkotf  20086  txcnp  20121  txcnmpt  20125  txrest  20132  txlm  20149  txflf  20507  dscmet  21093  xrtgioo  21311  ishtpy  21472  opnmblALT  22012  tglnfn  23934  numclwwlkdisj  25080  hlimreui  26157  ofoprabco  27505  dya2iocct  28251  sseqfv2  28333  ptrest  30048  rrnval  30323  atpsubN  35477
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618
This theorem depends on definitions:  df-bi 185  df-ral 2812
  Copyright terms: Public domain W3C validator