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

Theorem rgen2w 2829
Description: Generalization rule for restricted quantification. Note that  x and  y needn't be distinct. (Contributed by NM, 18-Jun-2014.)
Hypothesis
Ref Expression
rgenw.1  |-  ph
Assertion
Ref Expression
rgen2w  |-  A. x  e.  A  A. y  e.  B  ph

Proof of Theorem rgen2w
StepHypRef Expression
1 rgenw.1 . . 3  |-  ph
21rgenw 2828 . 2  |-  A. y  e.  B  ph
32rgenw 2828 1  |-  A. x  e.  A  A. y  e.  B  ph
Colors of variables: wff setvar class
Syntax hints:   A.wral 2817
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601
This theorem depends on definitions:  df-bi 185  df-ral 2822
This theorem is referenced by:  porpss  6578  fnmpt2i  6863  relmpt2opab  6875  cantnfvalf  8094  ixxf  11549  fzf  11686  fzof  11804  rexfiuz  13155  sadcf  13974  prdsval  14722  prdsds  14731  homfeq  14962  comfeq  14974  wunnat  15195  eldmcoa  15262  catcfuccl  15306  relxpchom  15320  catcxpccl  15346  plusffval  15746  lsmass  16538  efgval2  16592  dmdprd  16879  dprdval  16884  dprdvalOLD  16886  scaffval  17378  ipffval  18529  eltx  19914  xkotf  19931  txcnp  19966  txcnmpt  19970  txrest  19977  txlm  19994  txflf  20352  dscmet  20938  xrtgioo  21156  ishtpy  21317  opnmblALT  21857  tglnfn  23777  numclwwlkdisj  24872  hlimreui  25948  ofoprabco  27296  pstmxmet  27669  dya2iocct  28044  sseqfv2  28126  ptrest  29943  rrnval  30218  atpsubN  34842
  Copyright terms: Public domain W3C validator