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

Theorem rgen2 2639
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 2626 . 2  |-  ( x  e.  A  ->  A. y  e.  B  ph )
32rgen 2608 1  |-  A. x  e.  A  A. y  e.  B  ph
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1684   A.wral 2543
This theorem is referenced by:  rgen3  2640  f1stres  6141  f2ndres  6142  smobeth  8208  smupf  12669  xpsff1o  13470  sscres  13700  efgmf  15022  efglem  15025  txuni2  17260  divcn  18372  abscncf  18405  recncf  18406  imcncf  18407  cjcncf  18408  cnllycmp  18454  bndth  18456  dyadf  18946  cxpcn3  20088  sgmf  20383  smcnlem  21270  helch  21823  hsn0elch  21827  hhshsslem2  21845  shscli  21896  shintcli  21908  0cnop  22559  0cnfn  22560  idcnop  22561  lnophsi  22581  nlelshi  22640  cnlnadjlem6  22652  cnllyscon  23187  rellyscon  23193  basexre  24934  1cat  25171  fneref  25696  frmx  26410  frmy  26411
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1532  df-ral 2548
  Copyright terms: Public domain W3C validator