Theorem abssi 4021

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

Syntax hints:   → wi 4   ∈ wcel 2142  {cab 2740   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ss 3921

This theorem is referenced by:  ssab2  4032  intab  4936  opabss  5164  abex  5282  relopabiALT  5796  exse2  7898  opiota  8040  mpoexw  8059  fsplitfpar  8097  tfrlem8  8355  fiprc  9025  fival  9358  hartogslem1  9490  dmttrcl  9676  rnttrcl  9677  tz9.12lem1  9745  rankuni  9821  scott0  9844  r0weon  9968  alephval3  10066  aceq3lem  10076  dfac5lem4  10082  dfac5lem4OLD  10084  dfac2b  10087  cff  10204  cfsuc  10214  cff1  10215  cflim2  10220  cfss  10222  axdc3lem  10407  axdclem  10476  gruina  10776  nqpr  10972  infcvgaux1i  15887  4sqlem1  16984  sscpwex  17848  cssval  21734  topnex  23056  islocfin  23577  hauspwpwf1  24047  itg2lcl  25789  2sqlem7  27488  cutsf  27885  isismt  28703  nmcexi  32229  opabssi  32815  lsmsnorb  33577  dispcmp  34156  cnre2csqima  34208  mppspstlem  35921  colinearex  36410  itg2addnclem  38170  itg2addnc  38173  eldiophb  43338