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

Theorem rsp2 2831
Description: Restricted specialization, with two quantifiers. (Contributed by NM, 11-Feb-1997.)
Assertion
Ref Expression
rsp2

Proof of Theorem rsp2
StepHypRef Expression
1 rsp 2823 . . 3
2 rsp 2823 . . 3
31, 2syl6 33 . 2
43impd 431 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818  A.wral 2807
This theorem is referenced by:  ralcom2  3022  disjxiun  4449  solin  4828  mpt2curryd  7017  cmncom  16814  cnmpt21  20172  cnmpt2t  20174  cnmpt22  20175  cnmptcom  20179  frgrawopreglem5  25048  subgoablo  25313  htthlem  25834  prtlem14  30615  islptre  31625
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-ral 2812
  Copyright terms: Public domain W3C validator