Theorem abssi 4080

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

Syntax hints:   → wi 4   ∈ wcel 2106  {cab 2712   ⊆ wss 3963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ss 3980

This theorem is referenced by:  ssab2  4089  intab  4983  opabss  5212  relopabiALT  5836  exse2  7940  opiota  8083  mpoexw  8102  fsplitfpar  8142  tfrlem8  8423  fiprc  9084  fival  9450  hartogslem1  9580  dmttrcl  9759  rnttrcl  9760  tz9.12lem1  9825  rankuni  9901  scott0  9924  r0weon  10050  alephval3  10148  aceq3lem  10158  dfac5lem4  10164  dfac5lem4OLD  10166  dfac2b  10169  cff  10286  cfsuc  10295  cff1  10296  cflim2  10301  cfss  10303  axdc3lem  10488  axdclem  10557  gruina  10856  nqpr  11052  infcvgaux1i  15890  4sqlem1  16982  sscpwex  17863  cssval  21718  topnex  23019  islocfin  23541  hauspwpwf1  24011  itg2lcl  25777  2sqlem7  27483  scutf  27872  isismt  28557  nmcexi  32055  opabssi  32633  lsmsnorb  33399  dispcmp  33820  cnre2csqima  33872  mppspstlem  35556  colinearex  36042  itg2addnclem  37658  itg2addnc  37661  eldiophb  42745