Theorem abssi 4015

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 4013	. 2 ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝑥 ∈ 𝐴}
3		abid2 2868	. 2 ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴
4	2, 3	sseqtri 3978	1 ⊢ {𝑥 ∣ 𝜑} ⊆ 𝐴

Syntax hints:   → wi 4   ∈ wcel 2111  {cab 2709   ⊆ wss 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ss 3914

This theorem is referenced by:  ssab2  4026  intab  4926  opabss  5153  relopabiALT  5762  exse2  7847  opiota  7991  mpoexw  8010  fsplitfpar  8048  tfrlem8  8303  fiprc  8966  fival  9296  hartogslem1  9428  dmttrcl  9611  rnttrcl  9612  tz9.12lem1  9680  rankuni  9756  scott0  9779  r0weon  9903  alephval3  10001  aceq3lem  10011  dfac5lem4  10017  dfac5lem4OLD  10019  dfac2b  10022  cff  10139  cfsuc  10148  cff1  10149  cflim2  10154  cfss  10156  axdc3lem  10341  axdclem  10410  gruina  10709  nqpr  10905  infcvgaux1i  15764  4sqlem1  16860  sscpwex  17722  cssval  21619  topnex  22911  islocfin  23432  hauspwpwf1  23902  itg2lcl  25655  2sqlem7  27362  scutf  27753  isismt  28512  nmcexi  32006  opabssi  32596  lsmsnorb  33356  dispcmp  33872  cnre2csqima  33924  mppspstlem  35615  colinearex  36104  itg2addnclem  37721  itg2addnc  37724  eldiophb  42860