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

Theorem rgen2w 3066
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 3065 . 2 𝑦𝐵 𝜑
32rgenw 3065 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 1795
This theorem depends on definitions:  df-bi 207  df-ral 3062
This theorem is referenced by:  porpss  7747  fnmpoi  8095  mptmpoopabbrd  8105  relmpoopab  8119  cantnfvalf  9705  ixxf  13397  fzf  13551  fzof  13696  rexfiuz  15386  sadcf  16490  prdsvallem  17499  prdsds  17509  homfeq  17737  comfeq  17749  wunnat  18004  eldmcoa  18110  catcfuccl  18163  relxpchom  18226  catcxpccl  18252  plusffval  18659  grpsubfval  19001  lsmass  19687  efgval2  19742  dmdprd  20018  dprdval  20023  scaffval  20878  ipffval  21666  psdmul  22170  eltx  23576  xkotf  23593  txcnp  23628  txcnmpt  23632  txrest  23639  txlm  23656  txflf  24014  dscmet  24585  xrtgioo  24828  ishtpy  25004  opnmblALT  25638  tglnfn  28555  wwlksonvtx  29875  wspthnonp  29879  clwwlknondisj  30130  hlimreui  31258  aciunf1lem  32672  ofoprabco  32674  lsmssass  33430  dya2iocct  34282  icoreresf  37353  curfv  37607  ptrest  37626  poimirlem26  37653  rrnval  37834  atpsubN  39755  clsk3nimkb  44053  2arymaptf1  48574
  Copyright terms: Public domain W3C validator