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

Theorem rgen2 2812
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 2799 . 2  |-  ( x  e.  A  ->  A. y  e.  B  ph )
32rgen 2781 1  |-  A. x  e.  A  A. y  e.  B  ph
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1756   A.wral 2715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-ral 2720
This theorem is referenced by:  rgen3  2813  f1stres  6598  f2ndres  6599  smobeth  8750  disjxwrd  12349  wrd2ind  12372  smupf  13674  xpsff1o  14506  efgmf  16210  efglem  16213  nn0srg  17881  rge0srg  17882  txuni2  19138  divcn  20444  abscncf  20477  recncf  20478  imcncf  20479  cjcncf  20480  cnllycmp  20528  bndth  20530  dyadf  21071  cxpcn3  22186  sgmf  22483  ercgrg  22969  smcnlem  24092  helch  24646  hsn0elch  24651  hhshsslem2  24669  shscli  24720  shintcli  24732  0cnop  25383  0cnfn  25384  idcnop  25385  lnophsi  25405  nlelshi  25464  cnlnadjlem6  25476  cnllyscon  27134  rellyscon  27140  mblfinlem1  28428  mblfinlem2  28429  fneref  28556  frmx  29254  frmy  29255  ldepslinc  31051
  Copyright terms: Public domain W3C validator