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

Theorem rgen2w 2774
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 2773 . 2  |-  A. y  e.  B  ph
32rgenw 2773 1  |-  A. x  e.  A  A. y  e.  B  ph
Colors of variables: wff set class
Syntax hints:   A.wral 2705
This theorem is referenced by:  fnmpt2i  6420  relmpt2opab  6429  porpss  6526  cantnfvalf  7620  ixxf  10926  fzf  11047  fzof  11137  rexfiuz  12151  sadcf  12965  prdsval  13678  prdsds  13686  homfeq  13920  comfeq  13932  wunnat  14153  eldmcoa  14220  catcfuccl  14264  relxpchom  14278  catcxpccl  14304  plusffval  14702  lsmass  15302  efgval2  15356  dmdprd  15559  dprdval  15561  scaffval  15968  ipffval  16879  eltx  17600  xkotf  17617  txcnp  17652  txcnmpt  17656  txrest  17663  txlm  17680  txflf  18038  dscmet  18620  xrtgioo  18837  ishtpy  18997  opnmblALT  19495  hlimreui  22742  ofoprabco  24079  pstmxmet  24292  dya2iocct  24630  rrnval  26536  atpsubN  30550
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555
This theorem depends on definitions:  df-bi 178  df-ral 2710
  Copyright terms: Public domain W3C validator