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

Theorem rgen2w 2717
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 2716 . 2  |-  A. y  e.  B  ph
32rgenw 2716 1  |-  A. x  e.  A  A. y  e.  B  ph
Colors of variables: wff set class
Syntax hints:   A.wral 2649
This theorem is referenced by:  fnmpt2i  6359  relmpt2opab  6368  porpss  6462  cantnfvalf  7553  ixxf  10858  fzf  10979  fzof  11067  rexfiuz  12078  sadcf  12892  prdsval  13605  prdsds  13613  homfeq  13847  comfeq  13859  wunnat  14080  eldmcoa  14147  catcfuccl  14191  relxpchom  14205  catcxpccl  14231  plusffval  14629  lsmass  15229  efgval2  15283  dmdprd  15486  dprdval  15488  scaffval  15895  ipffval  16802  eltx  17521  xkotf  17538  txcnp  17573  txcnmpt  17577  txrest  17584  txlm  17601  txflf  17959  dscmet  18491  xrtgioo  18708  ishtpy  18868  opnmblALT  19362  hlimreui  22590  ofoprabco  23921  dya2iocct  24424  rrnval  26227  atpsubN  29867
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 2654
  Copyright terms: Public domain W3C validator