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

Theorem rgen2w 3077
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 3076 . 2 𝑦𝐵 𝜑
32rgenw 3076 1 𝑥𝐴𝑦𝐵 𝜑
Colors of variables: wff setvar class
Syntax hints:  wral 3064
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873
This theorem depends on definitions:  df-bi 198  df-ral 3069
This theorem is referenced by:  porpss  7109  fnmpt2i  7410  relmpt2opab  7431  cantnfvalf  8747  ixxf  12409  fzf  12559  fzof  12697  rexfiuz  14317  sadcf  15404  prdsval  16343  prdsds  16352  homfeq  16581  comfeq  16593  wunnat  16843  eldmcoa  16942  catcfuccl  16986  relxpchom  17049  catcxpccl  17075  plusffval  17475  lsmass  18310  efgval2  18364  dmdprd  18625  dprdval  18630  scaffval  19111  ipffval  20230  eltx  21612  xkotf  21629  txcnp  21664  txcnmpt  21668  txrest  21675  txlm  21692  txflf  22050  dscmet  22617  xrtgioo  22849  ishtpy  23011  opnmblALT  23611  tglnfn  25684  wwlksonvtx  27006  wspthnonp  27014  clwwlknondisj  27308  clwwlknondisjOLD  27313  hlimreui  28453  aciunf1lem  29819  ofoprabco  29821  dya2iocct  30699  icoreresf  33554  curfv  33739  ptrest  33758  poimirlem26  33785  rrnval  33974  atpsubN  35577  clsk3nimkb  38878
  Copyright terms: Public domain W3C validator