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

Theorem rgen2w 2776
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 2775 . 2  |-  A. y  e.  B  ph
32rgenw 2775 1  |-  A. x  e.  A  A. y  e.  B  ph
Colors of variables: wff setvar class
Syntax hints:   A.wral 2707
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596
This theorem depends on definitions:  df-bi 185  df-ral 2712
This theorem is referenced by:  porpss  6355  fnmpt2i  6634  relmpt2opab  6646  cantnfvalf  7863  ixxf  11300  fzf  11430  fzof  11536  rexfiuz  12821  sadcf  13634  prdsval  14378  prdsds  14387  homfeq  14618  comfeq  14630  wunnat  14851  eldmcoa  14918  catcfuccl  14962  relxpchom  14976  catcxpccl  15002  plusffval  15412  lsmass  16149  efgval2  16203  dmdprd  16456  dprdval  16461  dprdvalOLD  16463  scaffval  16892  ipffval  17921  eltx  18985  xkotf  19002  txcnp  19037  txcnmpt  19041  txrest  19048  txlm  19065  txflf  19423  dscmet  20009  xrtgioo  20227  ishtpy  20388  opnmblALT  20927  tglnfn  22864  hlimreui  24467  ofoprabco  25808  pstmxmet  26180  dya2iocct  26551  sseqfv2  26627  ptrest  28271  rrnval  28572  numclwwlkdisj  30521  atpsubN  33010
  Copyright terms: Public domain W3C validator