Theorem abssi 4032

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

Syntax hints:   → wi 4   ∈ wcel 2106  {cab 2708   ⊆ wss 3913

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930

This theorem is referenced by:  ssab2  4041  intab  4944  opabss  5174  relopabiALT  5784  exse2  7859  opiota  7996  mpoexw  8016  fsplitfpar  8055  tfrlem8  8335  fiprc  8996  fival  9357  hartogslem1  9487  dmttrcl  9666  rnttrcl  9667  tz9.12lem1  9732  rankuni  9808  scott0  9831  r0weon  9957  alephval3  10055  aceq3lem  10065  dfac5lem4  10071  dfac2b  10075  cff  10193  cfsuc  10202  cff1  10203  cflim2  10208  cfss  10210  axdc3lem  10395  axdclem  10464  gruina  10763  nqpr  10959  infcvgaux1i  15753  4sqlem1  16831  sscpwex  17712  cssval  21123  topnex  22383  islocfin  22905  hauspwpwf1  23375  itg2lcl  25129  2sqlem7  26809  scutf  27194  isismt  27539  nmcexi  31031  opabssi  31599  lsmsnorb  32245  dispcmp  32529  cnre2csqima  32581  mppspstlem  34252  colinearex  34721  itg2addnclem  36202  itg2addnc  36205  eldiophb  41138