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 1870
This theorem depends on definitions:  df-bi 197  df-ral 3066
This theorem is referenced by:  porpss  7086  fnmpt2i  7387  relmpt2opab  7408  cantnfvalf  8724  ixxf  12383  fzf  12530  fzof  12668  rexfiuz  14288  sadcf  15376  prdsval  16316  prdsds  16325  homfeq  16554  comfeq  16566  wunnat  16816  eldmcoa  16915  catcfuccl  16959  relxpchom  17022  catcxpccl  17048  plusffval  17448  lsmass  18283  efgval2  18337  dmdprd  18598  dprdval  18603  scaffval  19084  ipffval  20203  eltx  21585  xkotf  21602  txcnp  21637  txcnmpt  21641  txrest  21648  txlm  21665  txflf  22023  dscmet  22590  xrtgioo  22822  ishtpy  22984  opnmblALT  23584  tglnfn  25656  wwlksonvtx  26978  wspthnonp  26986  clwwlknondisj  27280  clwwlknondisjOLD  27285  hlimreui  28429  aciunf1lem  29795  ofoprabco  29797  dya2iocct  30675  icoreresf  33530  curfv  33715  ptrest  33734  poimirlem26  33761  rrnval  33951  atpsubN  35554  clsk3nimkb  38857
  Copyright terms: Public domain W3C validator