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

Theorem rsp2 2605
Description: Restricted specialization. (Contributed by NM, 11-Feb-1997.)
Assertion
Ref Expression
rsp2  |-  ( A. x  e.  A  A. y  e.  B  ph  ->  ( ( x  e.  A  /\  y  e.  B
)  ->  ph ) )

Proof of Theorem rsp2
StepHypRef Expression
1 rsp 2603 . . 3  |-  ( A. x  e.  A  A. y  e.  B  ph  ->  ( x  e.  A  ->  A. y  e.  B  ph ) )
2 rsp 2603 . . 3  |-  ( A. y  e.  B  ph  ->  ( y  e.  B  ->  ph ) )
31, 2syl6 29 . 2  |-  ( A. x  e.  A  A. y  e.  B  ph  ->  ( x  e.  A  -> 
( y  e.  B  ->  ph ) ) )
43imp3a 420 1  |-  ( A. x  e.  A  A. y  e.  B  ph  ->  ( ( x  e.  A  /\  y  e.  B
)  ->  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1684   A.wral 2543
This theorem is referenced by:  ralcom2  2704  disjxiun  4020  solin  4337  f1fveq  5786  cmncom  15105  cnmpt21  17365  cnmpt2t  17367  cnmpt22  17368  cnmptcom  17372  subgoablo  20978  htthlem  21497  ismonc  25814  iepiclem  25823  isepic  25824  prtlem14  26742
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-ral 2548
  Copyright terms: Public domain W3C validator