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

Theorem rgen2w 2734
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 2733 . 2  |-  A. y  e.  B  ph
32rgenw 2733 1  |-  A. x  e.  A  A. y  e.  B  ph
Colors of variables: wff set class
Syntax hints:   A.wral 2666
This theorem is referenced by:  fnmpt2i  6379  relmpt2opab  6388  porpss  6485  cantnfvalf  7576  ixxf  10882  fzf  11003  fzof  11092  rexfiuz  12106  sadcf  12920  prdsval  13633  prdsds  13641  homfeq  13875  comfeq  13887  wunnat  14108  eldmcoa  14175  catcfuccl  14219  relxpchom  14233  catcxpccl  14259  plusffval  14657  lsmass  15257  efgval2  15311  dmdprd  15514  dprdval  15516  scaffval  15923  ipffval  16834  eltx  17553  xkotf  17570  txcnp  17605  txcnmpt  17609  txrest  17616  txlm  17633  txflf  17991  dscmet  18573  xrtgioo  18790  ishtpy  18950  opnmblALT  19448  hlimreui  22695  ofoprabco  24032  pstmxmet  24245  dya2iocct  24583  rrnval  26426  atpsubN  30235
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552
This theorem depends on definitions:  df-bi 178  df-ral 2671
  Copyright terms: Public domain W3C validator