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

Theorem rgen2w 3119
 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 3118 . 2 𝑦𝐵 𝜑
32rgenw 3118 1 𝑥𝐴𝑦𝐵 𝜑
 Colors of variables: wff setvar class Syntax hints:  ∀wral 3106 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797 This theorem depends on definitions:  df-bi 210  df-ral 3111 This theorem is referenced by:  porpss  7436  fnmpoi  7753  relmpoopab  7775  cantnfvalf  9115  ixxf  12739  fzf  12892  fzof  13033  rexfiuz  14702  sadcf  15795  prdsval  16723  prdsds  16732  homfeq  16959  comfeq  16971  wunnat  17221  eldmcoa  17320  catcfuccl  17364  relxpchom  17426  catcxpccl  17452  plusffval  17853  grpsubfval  18143  lsmass  18791  efgval2  18846  dmdprd  19117  dprdval  19122  scaffval  19649  ipffval  20342  eltx  22183  xkotf  22200  txcnp  22235  txcnmpt  22239  txrest  22246  txlm  22263  txflf  22621  dscmet  23189  xrtgioo  23421  ishtpy  23587  opnmblALT  24217  tglnfn  26351  wwlksonvtx  27651  wspthnonp  27655  clwwlknondisj  27906  hlimreui  29032  aciunf1lem  30435  ofoprabco  30437  lsmssass  31019  dya2iocct  31663  icoreresf  34788  curfv  35056  ptrest  35075  poimirlem26  35102  rrnval  35284  atpsubN  37068  clsk3nimkb  40786  2arymaptf1  45108
 Copyright terms: Public domain W3C validator