ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  rgen2 Unicode version

Theorem rgen2 2592
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 2579 . 2  |-  ( x  e.  A  ->  A. y  e.  B  ph )
32rgen 2559 1  |-  A. x  e.  A  A. y  e.  B  ph
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    e. wcel 2176   A.wral 2484
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-gen 1472  ax-4 1533  ax-17 1549
This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489
This theorem is referenced by:  rgen3  2593  f1stres  6245  f2ndres  6246  exmidonfinlem  7301  netap  7366  2onetap  7367  2omotaplemap  7369  mpomulf  8062  aptap  8723  divfnzn  9742  1arith  12690  xpsff1o  13181  mgmidmo  13204  nmznsg  13549  isabli  13636  rhmfn  13934  cnsubmlem  14340  cnsubrglem  14342  txuni2  14728  divcnap  15037  abscncf  15057  recncf  15058  imcncf  15059  cjcncf  15060  reefiso  15249  ioocosf1o  15326  sgmf  15458  perfectlem2  15472  2lgslem1b  15566
  Copyright terms: Public domain W3C validator