Theorem abssi 3323

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 3320	. 2 |- { x | ph } C_ { x | x e. A }
3		abid2 2361	. 2 |- { x | x e. A } = A
4	2, 3	sseqtri 3282	1 |- { x | ph } C_ A

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   {cab 2224   C_ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-in 3226  df-ss 3233

This theorem is used by:  ssab2  3332  abf  3570  intab  3999  opabss  4195  relopabi  4905  exse2  5161  mpoexw  6449  tfrlem8  6589  frecabex  6669  fiprc  7104  fival  7304  nqprxx  7913  ltnqex  7916  gtnqex  7917  recexprlemell  7989  recexprlemelu  7990  recexprlempr  7999  4sqlem1  13167  topnex  15187  2sqlem7  16240