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

Theorem rgen2w 2909
 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 2908 . 2 𝑦𝐵 𝜑
32rgenw 2908 1 𝑥𝐴𝑦𝐵 𝜑
 Colors of variables: wff setvar class Syntax hints:  ∀wral 2896 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713 This theorem depends on definitions:  df-bi 196  df-ral 2901 This theorem is referenced by:  porpss  6839  fnmpt2i  7128  relmpt2opab  7146  cantnfvalf  8445  ixxf  12056  fzf  12201  fzof  12336  rexfiuz  13935  sadcf  15013  prdsval  15938  prdsds  15947  homfeq  16177  comfeq  16189  wunnat  16439  eldmcoa  16538  catcfuccl  16582  relxpchom  16644  catcxpccl  16670  plusffval  17070  lsmass  17906  efgval2  17960  dmdprd  18220  dprdval  18225  scaffval  18704  ipffval  19812  eltx  21181  xkotf  21198  txcnp  21233  txcnmpt  21237  txrest  21244  txlm  21261  txflf  21620  dscmet  22187  xrtgioo  22417  ishtpy  22579  opnmblALT  23177  tglnfn  25242  numclwwlkdisj  26607  hlimreui  27480  aciunf1lem  28844  ofoprabco  28847  dya2iocct  29669  sseqfv2  29783  icoreresf  32376  curfv  32559  ptrest  32578  poimirlem26  32605  rrnval  32796  atpsubN  34057  clsk3nimkb  37358  wspthnonp  41055  clwwlksndisj  41280
 Copyright terms: Public domain W3C validator