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

Theorem rgen2w 3148
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 3147 . 2 𝑦𝐵 𝜑
32rgenw 3147 1 𝑥𝐴𝑦𝐵 𝜑
Colors of variables: wff setvar class
Syntax hints:  wral 3135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787
This theorem depends on definitions:  df-bi 208  df-ral 3140
This theorem is referenced by:  porpss  7442  fnmpoi  7757  relmpoopab  7778  cantnfvalf  9116  ixxf  12736  fzf  12884  fzof  13023  rexfiuz  14695  sadcf  15790  prdsval  16716  prdsds  16725  homfeq  16952  comfeq  16964  wunnat  17214  eldmcoa  17313  catcfuccl  17357  relxpchom  17419  catcxpccl  17445  plusffval  17846  grpsubfval  18085  lsmass  18724  efgval2  18779  dmdprd  19049  dprdval  19054  scaffval  19581  ipffval  20720  eltx  22104  xkotf  22121  txcnp  22156  txcnmpt  22160  txrest  22167  txlm  22184  txflf  22542  dscmet  23109  xrtgioo  23341  ishtpy  23503  opnmblALT  24131  tglnfn  26260  wwlksonvtx  27560  wspthnonp  27564  clwwlknondisj  27817  hlimreui  28943  aciunf1lem  30335  ofoprabco  30337  dya2iocct  31437  icoreresf  34515  curfv  34753  ptrest  34772  poimirlem26  34799  rrnval  34986  atpsubN  36769  clsk3nimkb  40268
  Copyright terms: Public domain W3C validator