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

Theorem abssi 3422
Description: Inference of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.)
Hypothesis
Ref Expression
abssi.1  |-  ( ph  ->  x  e.  A )
Assertion
Ref Expression
abssi  |-  { x  |  ph }  C_  A
Distinct variable group:    x, A
Allowed substitution hint:    ph( x)

Proof of Theorem abssi
StepHypRef Expression
1 abssi.1 . . 3  |-  ( ph  ->  x  e.  A )
21ss2abi 3419 . 2  |-  { x  |  ph }  C_  { x  |  x  e.  A }
3 abid2 2555 . 2  |-  { x  |  x  e.  A }  =  A
42, 3sseqtri 3383 1  |-  { x  |  ph }  C_  A
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   {cab 2424    C_ wss 3323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-in 3330  df-ss 3337
This theorem is referenced by:  ssab2  3431  abf  3666  intab  4153  opabss  4348  relopabi  4960  exse2  6512  opiota  6628  tfrlem8  6835  fiprc  7383  fival  7654  hartogslem1  7748  tz9.12lem1  7986  rankuni  8062  scott0  8085  r0weon  8171  alephval3  8272  aceq3lem  8282  dfac5lem4  8288  dfac2  8292  cff  8409  cfsuc  8418  cff1  8419  cflim2  8424  cfss  8426  axdc3lem  8611  axdclem  8680  gruina  8977  nqpr  9175  infcvgaux1i  13311  4sqlem1  14001  sscpwex  14720  symgval  15875  cssval  18082  hauspwpwf1  19535  itg2lcl  21180  2sqlem7  22684  nmcexi  25381  cnre2csqima  26293  colinearex  28042  itg2addnclem  28396  itg2addnc  28399  areacirc  28442  islocfin  28521  eldiophb  29048
  Copyright terms: Public domain W3C validator