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

Theorem rgen2w 2920
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 2919 . 2 𝑦𝐵 𝜑
32rgenw 2919 1 𝑥𝐴𝑦𝐵 𝜑
Colors of variables: wff setvar class
Syntax hints:  wral 2907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719
This theorem depends on definitions:  df-bi 197  df-ral 2912
This theorem is referenced by:  porpss  6901  fnmpt2i  7191  relmpt2opab  7211  cantnfvalf  8514  ixxf  12135  fzf  12280  fzof  12416  rexfiuz  14029  sadcf  15110  prdsval  16047  prdsds  16056  homfeq  16286  comfeq  16298  wunnat  16548  eldmcoa  16647  catcfuccl  16691  relxpchom  16753  catcxpccl  16779  plusffval  17179  lsmass  18015  efgval2  18069  dmdprd  18329  dprdval  18334  scaffval  18813  ipffval  19925  eltx  21294  xkotf  21311  txcnp  21346  txcnmpt  21350  txrest  21357  txlm  21374  txflf  21733  dscmet  22300  xrtgioo  22532  ishtpy  22694  opnmblALT  23294  tglnfn  25359  wspthnonp  26630  clwwlksndisj  26856  hlimreui  27966  aciunf1lem  29327  ofoprabco  29330  dya2iocct  30147  icoreresf  32867  curfv  33056  ptrest  33075  poimirlem26  33102  rrnval  33293  atpsubN  34554  clsk3nimkb  37855
  Copyright terms: Public domain W3C validator