Theorem abssi 4030

Description: Inference of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.)

Hypothesis

Ref	Expression
abssi.1	⊢ (𝜑 → 𝑥 ∈ 𝐴)

Assertion

Ref	Expression
abssi	⊢ {𝑥 ∣ 𝜑} ⊆ 𝐴

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem abssi

Step	Hyp	Ref	Expression
1		abssi.1	. . 3 ⊢ (𝜑 → 𝑥 ∈ 𝐴)
2	1	ss2abi 4028	. 2 ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝑥 ∈ 𝐴}
3		abid2 2906	. 2 ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴
4	2, 3	sseqtri 3993	1 ⊢ {𝑥 ∣ 𝜑} ⊆ 𝐴

Syntax hints:   → wi 4   ∈ wcel 2149  {cab 2747   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ss 3930

This theorem is referenced by:  ssab2  4041  intab  4947  opabss  5179  abex  5297  relopabiALT  5811  exse2  7913  opiota  8055  mpoexw  8074  fsplitfpar  8112  tfrlem8  8370  fiprc  9040  fival  9371  hartogslem1  9503  dmttrcl  9689  rnttrcl  9690  tz9.12lem1  9758  rankuni  9834  scott0  9859  r0weon  9995  alephval3  10093  aceq3lem  10103  dfac5lem4  10109  dfac2b  10113  cff  10230  cfsuc  10240  cff1  10241  cflim2  10246  cfss  10248  axdc3lem  10433  axdclem  10502  gruina  10802  nqpr  10998  infcvgaux1i  15910  4sqlem1  17007  sscpwex  17871  cssval  21800  topnex  23121  islocfin  23642  hauspwpwf1  24112  itg2lcl  25854  2sqlem7  27553  cutsf  27950  isismt  28768  nmcexi  32318  opabssi  32898  lsmsnorb  33647  dispcmp  34193  cnre2csqima  34245  mppspstlem  35961  colinearex  36450  itg2addnclem  38209  itg2addnc  38212  eldiophb  43379