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

Theorem rgen2w 3065
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 3064 . 2 𝑦𝐵 𝜑
32rgenw 3064 1 𝑥𝐴𝑦𝐵 𝜑
Colors of variables: wff setvar class
Syntax hints:  wral 3060
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 206  df-ral 3061
This theorem is referenced by:  porpss  7700  fnmpoi  8038  relmpoopab  8062  cantnfvalf  9642  ixxf  13316  fzf  13470  fzof  13611  rexfiuz  15276  sadcf  16376  prdsvallem  17382  prdsds  17392  homfeq  17620  comfeq  17632  wunnat  17889  wunnatOLD  17890  eldmcoa  17997  catcfuccl  18051  catcfucclOLD  18052  relxpchom  18115  catcxpccl  18141  catcxpcclOLD  18142  plusffval  18549  grpsubfval  18843  lsmass  19501  efgval2  19556  dmdprd  19827  dprdval  19832  scaffval  20439  ipffval  21134  eltx  23001  xkotf  23018  txcnp  23053  txcnmpt  23057  txrest  23064  txlm  23081  txflf  23439  dscmet  24010  xrtgioo  24251  ishtpy  24417  opnmblALT  25049  tglnfn  27663  wwlksonvtx  28974  wspthnonp  28978  clwwlknondisj  29229  hlimreui  30355  aciunf1lem  31756  ofoprabco  31758  lsmssass  32370  dya2iocct  33110  icoreresf  36037  curfv  36272  ptrest  36291  poimirlem26  36318  rrnval  36500  atpsubN  38429  clsk3nimkb  42562  2arymaptf1  46987
  Copyright terms: Public domain W3C validator