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

Theorem rgen2w 3074
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 3073 . 2 𝑦𝐵 𝜑
32rgenw 3073 1 𝑥𝐴𝑦𝐵 𝜑
Colors of variables: wff setvar class
Syntax hints:  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803
This theorem depends on definitions:  df-bi 210  df-ral 3066
This theorem is referenced by:  porpss  7515  fnmpoi  7840  relmpoopab  7862  cantnfvalf  9280  ixxf  12945  fzf  13099  fzof  13240  rexfiuz  14911  sadcf  16012  prdsvallem  16959  prdsds  16969  homfeq  17197  comfeq  17209  wunnat  17463  wunnatOLD  17464  eldmcoa  17571  catcfuccl  17625  catcfucclOLD  17626  relxpchom  17688  catcxpccl  17714  catcxpcclOLD  17715  plusffval  18120  grpsubfval  18411  lsmass  19059  efgval2  19114  dmdprd  19385  dprdval  19390  scaffval  19917  ipffval  20610  eltx  22465  xkotf  22482  txcnp  22517  txcnmpt  22521  txrest  22528  txlm  22545  txflf  22903  dscmet  23470  xrtgioo  23703  ishtpy  23869  opnmblALT  24500  tglnfn  26638  wwlksonvtx  27939  wspthnonp  27943  clwwlknondisj  28194  hlimreui  29320  aciunf1lem  30719  ofoprabco  30721  lsmssass  31304  dya2iocct  31959  icoreresf  35260  curfv  35494  ptrest  35513  poimirlem26  35540  rrnval  35722  atpsubN  37504  clsk3nimkb  41327  2arymaptf1  45672
  Copyright terms: Public domain W3C validator