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

Theorem rgen2w 2954
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 2953 . 2 𝑦𝐵 𝜑
32rgenw 2953 1 𝑥𝐴𝑦𝐵 𝜑
Colors of variables: wff setvar class
Syntax hints:  wral 2941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762
This theorem depends on definitions:  df-bi 197  df-ral 2946
This theorem is referenced by:  porpss  6983  fnmpt2i  7284  relmpt2opab  7304  cantnfvalf  8600  ixxf  12223  fzf  12368  fzof  12506  rexfiuz  14131  sadcf  15222  prdsval  16162  prdsds  16171  homfeq  16401  comfeq  16413  wunnat  16663  eldmcoa  16762  catcfuccl  16806  relxpchom  16868  catcxpccl  16894  plusffval  17294  lsmass  18129  efgval2  18183  dmdprd  18443  dprdval  18448  scaffval  18929  ipffval  20041  eltx  21419  xkotf  21436  txcnp  21471  txcnmpt  21475  txrest  21482  txlm  21499  txflf  21857  dscmet  22424  xrtgioo  22656  ishtpy  22818  opnmblALT  23417  tglnfn  25487  wwlksonvtx  26805  wspthnonp  26813  clwwlknondisj  27086  clwwlknondisjOLD  27090  hlimreui  28224  aciunf1lem  29590  ofoprabco  29592  dya2iocct  30470  icoreresf  33330  curfv  33519  ptrest  33538  poimirlem26  33565  rrnval  33756  atpsubN  35357  clsk3nimkb  38655
  Copyright terms: Public domain W3C validator