Theorem abssi 4016

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  {cab 2738   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3916

This theorem is used by:  ssab2  4027  intab  4938  opabss  5169  abex  5291  relopabiALT  5804  exse2  7915  opiota  8057  mpoexw  8078  fsplitfpar  8116  tfrlem8  8374  fiprc  9052  fival  9383  hartogslem1  9515  dmttrcl  9701  rnttrcl  9702  tz9.12lem1  9770  rankuni  9846  scott0b  9877  scott0OLD  9878  r0weon  10016  alephval3  10114  aceq3lem  10124  dfac5lem4  10130  dfac2b  10134  cff  10250  cfsuc  10260  cff1  10261  cflim2  10266  cfss  10268  axdc3lem  10453  axdclem  10522  gruina  10828  nqpr  11024  infcvgaux1i  15947  4sqlem1  17041  sscpwex  17905  cssval  21896  topnex  23222  islocfin  23744  hauspwpwf1  24214  itg2lcl  25956  2sqlem7  27661  cutsf  28058  isismt  28877  nmcexi  32508  opabssi  33087  lsmsnorb  33825  dispcmp  34370  cnre2csqima  34422  mppspstlem  36151  colinearex  36641  itg2addnclem  38421  itg2addnc  38424  eldiophb  43603