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

Theorem rgen2 2866
Description: Generalization rule for restricted quantification, with two quantifiers. (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 2855 . 2  |-  ( x  e.  A  ->  A. y  e.  B  ph )
32rgen 2801 1  |-  A. x  e.  A  A. y  e.  B  ph
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1802   A.wral 2791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689
This theorem depends on definitions:  df-bi 185  df-an 371  df-ral 2796
This theorem is referenced by:  rgen3  2867  f1stres  6804  f2ndres  6805  smobeth  8961  disjxwrd  12656  wrd2ind  12679  smupf  14002  xpsff1o  14839  efgmf  16602  efglem  16605  txuni2  19936  divcn  21242  abscncf  21275  recncf  21276  imcncf  21277  cjcncf  21278  cnllycmp  21326  bndth  21328  dyadf  21870  cxpcn3  22991  sgmf  23288  smcnlem  25476  helch  26030  hsn0elch  26035  hhshsslem2  26053  shscli  26104  shintcli  26116  0cnop  26767  0cnfn  26768  idcnop  26769  lnophsi  26789  nlelshi  26848  cnlnadjlem6  26860  cnzh  27821  rezh  27822  cnllyscon  28560  rellyscon  28566  mblfinlem1  30023  mblfinlem2  30024  fneref  30140  frmx  30821  frmy  30822  2zrngnmrid  32463  ldepslinc  32840
  Copyright terms: Public domain W3C validator