Theorem abssi 4009

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

Syntax hints:   → wi 4   ∈ wcel 2114  {cab 2715   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3907

This theorem is referenced by:  ssab2  4020  intab  4921  opabss  5150  abex  5264  relopabiALT  5773  exse2  7862  opiota  8006  mpoexw  8025  fsplitfpar  8062  tfrlem8  8317  fiprc  8985  fival  9319  hartogslem1  9451  dmttrcl  9636  rnttrcl  9637  tz9.12lem1  9705  rankuni  9781  scott0  9804  r0weon  9928  alephval3  10026  aceq3lem  10036  dfac5lem4  10042  dfac5lem4OLD  10044  dfac2b  10047  cff  10164  cfsuc  10173  cff1  10174  cflim2  10179  cfss  10181  axdc3lem  10366  axdclem  10435  gruina  10735  nqpr  10931  infcvgaux1i  15816  4sqlem1  16913  sscpwex  17776  cssval  21675  topnex  22974  islocfin  23495  hauspwpwf1  23965  itg2lcl  25707  2sqlem7  27404  cutsf  27801  isismt  28619  nmcexi  32115  opabssi  32704  lsmsnorb  33469  dispcmp  34022  cnre2csqima  34074  mppspstlem  35772  colinearex  36261  itg2addnclem  38009  itg2addnc  38012  eldiophb  43206