Theorem abssi 4023

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  {cab 2743   ⊆ wss 3906

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ss 3923

This theorem is used by:  ssab2  4034  intab  4945  opabss  5177  abex  5299  relopabiALT  5812  exse2  7920  opiota  8062  mpoexw  8081  fsplitfpar  8119  tfrlem8  8377  fiprc  9048  fival  9379  hartogslem1  9511  dmttrcl  9697  rnttrcl  9698  tz9.12lem1  9766  rankuni  9842  scott0b  9873  scott0OLD  9874  r0weon  10012  alephval3  10110  aceq3lem  10120  dfac5lem4  10126  dfac2b  10130  cff  10246  cfsuc  10256  cff1  10257  cflim2  10262  cfss  10264  axdc3lem  10449  axdclem  10518  gruina  10820  nqpr  11016  infcvgaux1i  15936  4sqlem1  17032  sscpwex  17896  cssval  21884  topnex  23205  islocfin  23727  hauspwpwf1  24197  itg2lcl  25939  2sqlem7  27641  cutsf  28038  isismt  28856  nmcexi  32451  opabssi  33031  lsmsnorb  33770  dispcmp  34315  cnre2csqima  34367  mppspstlem  36102  colinearex  36591  itg2addnclem  38381  itg2addnc  38384  eldiophb  43548