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

Theorem rgen2w 3151
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 3150 . 2 𝑦𝐵 𝜑
32rgenw 3150 1 𝑥𝐴𝑦𝐵 𝜑
Colors of variables: wff setvar class
Syntax hints:  wral 3138
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 3143
This theorem is referenced by:  porpss  7442  fnmpoi  7759  relmpoopab  7780  cantnfvalf  9117  ixxf  12738  fzf  12886  fzof  13025  rexfiuz  14697  sadcf  15792  prdsval  16718  prdsds  16727  homfeq  16954  comfeq  16966  wunnat  17216  eldmcoa  17315  catcfuccl  17359  relxpchom  17421  catcxpccl  17447  plusffval  17848  grpsubfval  18087  lsmass  18726  efgval2  18781  dmdprd  19051  dprdval  19056  scaffval  19583  ipffval  20722  eltx  22106  xkotf  22123  txcnp  22158  txcnmpt  22162  txrest  22169  txlm  22186  txflf  22544  dscmet  23111  xrtgioo  23343  ishtpy  23505  opnmblALT  24133  tglnfn  26261  wwlksonvtx  27561  wspthnonp  27565  clwwlknondisj  27818  hlimreui  28944  aciunf1lem  30336  ofoprabco  30338  dya2iocct  31438  icoreresf  34516  curfv  34754  ptrest  34773  poimirlem26  34800  rrnval  34988  atpsubN  36771  clsk3nimkb  40270
  Copyright terms: Public domain W3C validator