NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  sps Unicode version

Theorem sps 1754
Description: Generalization of antecedent. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
sps.1
Assertion
Ref Expression
sps

Proof of Theorem sps
StepHypRef Expression
1 sp 1747 . 2
2 sps.1 . 2
31, 2syl 15 1
Colors of variables: wff setvar class
Syntax hints:   wi 4  wal 1540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746
This theorem depends on definitions:  df-bi 177  df-ex 1542
This theorem is referenced by:  19.2g  1757  ax10lem4  1941  ax10lem6  1943  ax10o  1952  cbv1h  1978  equveli  1988  ax11v2  1992  drsb1  2022  dfsb2  2055  sbequi  2059  drsb2  2061  sbn  2062  sbi1  2063  nfsb4t  2080  sbco2  2086  sbcom  2089  sbcom2  2114  sbal1  2126  eujustALT  2207  mopick  2266  eupickbi  2270  ralcom2  2775  ceqsalg  2883  reu6  3025  sbcal  3093  csbie2t  3180  reldisj  3594  dfnfc2  3909  mosubopt  4612  ssopab2  4712  dfid3  4768  fununi  5160  fv3  5341  fnoprabg  5585  fundmen  6043
  Copyright terms: Public domain W3C validator