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

Theorem rgen2w 2784
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 2783 . 2  |-  A. y  e.  B  ph
32rgenw 2783 1  |-  A. x  e.  A  A. y  e.  B  ph
Colors of variables: wff setvar class
Syntax hints:   A.wral 2715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591
This theorem depends on definitions:  df-bi 185  df-ral 2720
This theorem is referenced by:  porpss  6364  fnmpt2i  6643  relmpt2opab  6655  cantnfvalf  7873  ixxf  11310  fzf  11441  fzof  11550  rexfiuz  12835  sadcf  13649  prdsval  14393  prdsds  14402  homfeq  14633  comfeq  14645  wunnat  14866  eldmcoa  14933  catcfuccl  14977  relxpchom  14991  catcxpccl  15017  plusffval  15427  lsmass  16167  efgval2  16221  dmdprd  16480  dprdval  16485  dprdvalOLD  16487  scaffval  16966  ipffval  18077  eltx  19141  xkotf  19158  txcnp  19193  txcnmpt  19197  txrest  19204  txlm  19221  txflf  19579  dscmet  20165  xrtgioo  20383  ishtpy  20544  opnmblALT  21083  tglnfn  22981  hlimreui  24642  ofoprabco  25982  pstmxmet  26324  dya2iocct  26695  sseqfv2  26777  ptrest  28425  rrnval  28726  numclwwlkdisj  30673  atpsubN  33397
  Copyright terms: Public domain W3C validator