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

Theorem rsp2 2618
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 2616 . . 3  |-  ( A. x  e.  A  A. y  e.  B  ph  ->  ( x  e.  A  ->  A. y  e.  B  ph ) )
2 rsp 2616 . . 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 1696   A.wral 2556
This theorem is referenced by:  ralcom2  2717  disjxiun  4036  solin  4353  f1fveq  5802  cmncom  15121  cnmpt21  17381  cnmpt2t  17383  cnmpt22  17384  cnmptcom  17388  subgoablo  20994  htthlem  21513  ismonc  25917  iepiclem  25926  isepic  25927  prtlem14  26845
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-ral 2561
  Copyright terms: Public domain W3C validator