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

Theorem rgen2w 2904
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 2903 . 2
32rgenw 2903 1
Colors of variables: wff setvar class
Syntax hints:  A.wral 2800
This theorem is referenced by:  porpss  6497  fnmpt2i  6776  relmpt2opab  6788  cantnfvalf  8010  ixxf  11449  fzf  11586  fzof  11695  rexfiuz  12993  sadcf  13807  prdsval  14552  prdsds  14561  homfeq  14792  comfeq  14804  wunnat  15025  eldmcoa  15092  catcfuccl  15136  relxpchom  15150  catcxpccl  15176  plusffval  15586  lsmass  16328  efgval2  16382  dmdprd  16655  dprdval  16660  dprdvalOLD  16662  scaffval  17142  ipffval  18270  eltx  19540  xkotf  19557  txcnp  19592  txcnmpt  19596  txrest  19603  txlm  19620  txflf  19978  dscmet  20564  xrtgioo  20782  ishtpy  20943  opnmblALT  21483  tglnfn  23398  hlimreui  25111  ofoprabco  26449  pstmxmet  26781  dya2iocct  27151  sseqfv2  27233  ptrest  28885  rrnval  29186  numclwwlkdisj  31550  atpsubN  34248
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592
This theorem depends on definitions:  df-bi 185  df-ral 2805
  Copyright terms: Public domain W3C validator