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

Theorem rgen2w 2624
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 2623 . 2  |-  A. y  e.  B  ph
32rgenw 2623 1  |-  A. x  e.  A  A. y  e.  B  ph
Colors of variables: wff set class
Syntax hints:   A.wral 2556
This theorem is referenced by:  fnmpt2i  6209  porpss  6297  cantnfvalf  7382  ixxf  10682  fzf  10802  fzof  10888  rexfiuz  11847  sadcf  12660  prdsval  13371  prdsds  13379  homfeq  13613  comfeq  13625  wunnat  13846  eldmcoa  13913  catcfuccl  13957  relxpchom  13971  1stfcl  13987  2ndfcl  13988  catcxpccl  13997  plusffval  14395  lsmass  14995  efgval2  15049  dmdprd  15252  dprdval  15254  scaffval  15661  ipffval  16568  eltx  17279  xkotf  17296  txcnp  17330  txcnmpt  17334  txrest  17341  txlm  17358  txflf  17717  dscmet  18111  xrtgioo  18328  ishtpy  18486  opnmblALT  18974  hlimreui  21835  ofoprabco  23247  dya2iocseg  23594  dya2iocct  23596  cbcpcp  25265  altretop  25703  rrnval  26654  atpsubN  30564
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536
This theorem depends on definitions:  df-bi 177  df-ral 2561
  Copyright terms: Public domain W3C validator