Theorem abssi 3677

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

Step	Hyp	Ref	Expression
1		abssi.1	. . 3 |- ( ph -> x e. A )
2	1	ss2abi 3674	. 2 |- { x | ph } C_ { x | x e. A }
3		abid2 2745	. 2 |- { x | x e. A } = A
4	2, 3	sseqtri 3637	1 |- { x | ph } C_ A

Syntax hints:   -> wi 4   e. wcel 1990   {cab 2608   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-in 3581  df-ss 3588

This theorem is referenced by:  ssab2  3686  intab  4507  opabss  4714  relopabiALT  5246  exse2  7105  opiota  7229  tfrlem8  7480  fiprc  8039  fival  8318  hartogslem1  8447  tz9.12lem1  8650  rankuni  8726  scott0  8749  r0weon  8835  alephval3  8933  aceq3lem  8943  dfac5lem4  8949  dfac2  8953  cff  9070  cfsuc  9079  cff1  9080  cflim2  9085  cfss  9087  axdc3lem  9272  axdclem  9341  gruina  9640  nqpr  9836  infcvgaux1i  14589  4sqlem1  15652  sscpwex  16475  symgval  17799  cssval  20026  topnex  20800  islocfin  21320  hauspwpwf1  21791  itg2lcl  23494  2sqlem7  25149  isismt  25429  nmcexi  28885  dispcmp  29926  cnre2csqima  29957  mppspstlem  31468  scutf  31919  colinearex  32167  itg2addnclem  33461  itg2addnc  33464  eldiophb  37320