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

Theorem rgen2 2652
Description: Generalization rule for restricted quantification. (Contributed by NM, 30-May-1999.)
Hypothesis
Ref Expression
rgen2.1  |-  ( ( x  e.  A  /\  y  e.  B )  ->  ph )
Assertion
Ref Expression
rgen2  |-  A. x  e.  A  A. y  e.  B  ph
Distinct variable groups:    x, y    y, A
Allowed substitution hints:    ph( x, y)    A( x)    B( x, y)

Proof of Theorem rgen2
StepHypRef Expression
1 rgen2.1 . . 3  |-  ( ( x  e.  A  /\  y  e.  B )  ->  ph )
21ralrimiva 2639 . 2  |-  ( x  e.  A  ->  A. y  e.  B  ph )
32rgen 2621 1  |-  A. x  e.  A  A. y  e.  B  ph
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1696   A.wral 2556
This theorem is referenced by:  rgen3  2653  f1stres  6157  f2ndres  6158  smobeth  8224  smupf  12685  xpsff1o  13486  sscres  13716  efgmf  15038  efglem  15041  txuni2  17276  divcn  18388  abscncf  18421  recncf  18422  imcncf  18423  cjcncf  18424  cnllycmp  18470  bndth  18472  dyadf  18962  cxpcn3  20104  sgmf  20399  smcnlem  21286  helch  21839  hsn0elch  21843  hhshsslem2  21861  shscli  21912  shintcli  21924  0cnop  22575  0cnfn  22576  idcnop  22577  lnophsi  22597  nlelshi  22656  cnlnadjlem6  22668  xrge0iifiso  23332  cnllyscon  23791  rellyscon  23797  basexre  25625  1cat  25862  fneref  26387  frmx  27101  frmy  27102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1535  df-ral 2561
  Copyright terms: Public domain W3C validator