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

Theorem rgen2w 2611
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 2610 . 2  |-  A. y  e.  B  ph
32rgenw 2610 1  |-  A. x  e.  A  A. y  e.  B  ph
Colors of variables: wff set class
Syntax hints:   A.wral 2543
This theorem is referenced by:  fnmpt2i  6193  porpss  6281  cantnfvalf  7366  ixxf  10666  fzf  10786  fzof  10872  rexfiuz  11831  sadcf  12644  prdsval  13355  prdsds  13363  homfeq  13597  comfeq  13609  wunnat  13830  eldmcoa  13897  catcfuccl  13941  relxpchom  13955  1stfcl  13971  2ndfcl  13972  catcxpccl  13981  plusffval  14379  lsmass  14979  efgval2  15033  dmdprd  15236  dprdval  15238  scaffval  15645  ipffval  16552  eltx  17263  xkotf  17280  txcnp  17314  txcnmpt  17318  txrest  17325  txlm  17342  txflf  17701  dscmet  18095  xrtgioo  18312  ishtpy  18470  opnmblALT  18958  hlimreui  21819  ofoprabco  23232  dya2iocseg  23579  dya2iocct  23581  cbcpcp  25162  altretop  25600  rrnval  26551  atpsubN  29942
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533
This theorem depends on definitions:  df-bi 177  df-ral 2548
  Copyright terms: Public domain W3C validator