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

Theorem rgen2 2802
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 2789 . 2  |-  ( x  e.  A  ->  A. y  e.  B  ph )
32rgen 2771 1  |-  A. x  e.  A  A. y  e.  B  ph
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1725   A.wral 2705
This theorem is referenced by:  rgen3  2803  f1stres  6368  f2ndres  6369  smobeth  8461  smupf  12990  xpsff1o  13793  efgmf  15345  efglem  15348  txuni2  17597  divcn  18898  abscncf  18931  recncf  18932  imcncf  18933  cjcncf  18934  cnllycmp  18981  bndth  18983  dyadf  19483  cxpcn3  20632  sgmf  20928  smcnlem  22193  helch  22746  hsn0elch  22750  hhshsslem2  22768  shscli  22819  shintcli  22831  0cnop  23482  0cnfn  23483  idcnop  23484  lnophsi  23504  nlelshi  23563  cnlnadjlem6  23575  cnllyscon  24932  rellyscon  24938  mblfinlem1  26243  mblfinlem2  26244  fneref  26364  frmx  26976  frmy  26977
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-ral 2710
  Copyright terms: Public domain W3C validator