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

Theorem rgen2w 2816
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 2815 . 2  |-  A. y  e.  B  ph
32rgenw 2815 1  |-  A. x  e.  A  A. y  e.  B  ph
Colors of variables: wff setvar class
Syntax hints:   A.wral 2804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623
This theorem depends on definitions:  df-bi 185  df-ral 2809
This theorem is referenced by:  porpss  6557  fnmpt2i  6842  relmpt2opab  6855  cantnfvalf  8075  ixxf  11542  fzf  11679  fzof  11801  rexfiuz  13262  sadcf  14187  prdsval  14944  prdsds  14953  homfeq  15182  comfeq  15194  wunnat  15444  eldmcoa  15543  catcfuccl  15587  relxpchom  15649  catcxpccl  15675  plusffval  16076  lsmass  16887  efgval2  16941  dmdprd  17224  dprdval  17229  dprdvalOLD  17231  scaffval  17725  ipffval  18856  eltx  20235  xkotf  20252  txcnp  20287  txcnmpt  20291  txrest  20298  txlm  20315  txflf  20673  dscmet  21259  xrtgioo  21477  ishtpy  21638  opnmblALT  22178  tglnfn  24135  numclwwlkdisj  25282  hlimreui  26355  aciunf1lem  27729  ofoprabco  27732  dya2iocct  28488  sseqfv2  28597  ptrest  30288  rrnval  30563  atpsubN  35874
  Copyright terms: Public domain W3C validator