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

Theorem rgen2 2889
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 2878 . 2  |-  ( x  e.  A  ->  A. y  e.  B  ph )
32rgen 2824 1  |-  A. x  e.  A  A. y  e.  B  ph
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1767   A.wral 2814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680
This theorem depends on definitions:  df-bi 185  df-an 371  df-ral 2819
This theorem is referenced by:  rgen3  2890  f1stres  6807  f2ndres  6808  smobeth  8962  disjxwrd  12646  wrd2ind  12669  smupf  13990  xpsff1o  14826  efgmf  16546  efglem  16549  nn0srg  18294  rge0srg  18295  fneref  19834  txuni2  19893  divcn  21199  abscncf  21232  recncf  21233  imcncf  21234  cjcncf  21235  cnllycmp  21283  bndth  21285  dyadf  21827  cxpcn3  22947  sgmf  23244  ercgrg  23733  smcnlem  25380  helch  25934  hsn0elch  25939  hhshsslem2  25957  shscli  26008  shintcli  26020  0cnop  26671  0cnfn  26672  idcnop  26673  lnophsi  26693  nlelshi  26752  cnlnadjlem6  26764  cnllyscon  28441  rellyscon  28447  mblfinlem1  29904  mblfinlem2  29905  frmx  30680  frmy  30681  ldepslinc  32408
  Copyright terms: Public domain W3C validator