Theorem abssi 4093

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

Syntax hints:   → wi 4   ∈ wcel 2108  {cab 2717   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ss 3993

This theorem is referenced by:  ssab2  4102  intab  5002  opabss  5230  relopabiALT  5847  exse2  7957  opiota  8100  mpoexw  8119  fsplitfpar  8159  tfrlem8  8440  fiprc  9111  fival  9481  hartogslem1  9611  dmttrcl  9790  rnttrcl  9791  tz9.12lem1  9856  rankuni  9932  scott0  9955  r0weon  10081  alephval3  10179  aceq3lem  10189  dfac5lem4  10195  dfac5lem4OLD  10197  dfac2b  10200  cff  10317  cfsuc  10326  cff1  10327  cflim2  10332  cfss  10334  axdc3lem  10519  axdclem  10588  gruina  10887  nqpr  11083  infcvgaux1i  15905  4sqlem1  16995  sscpwex  17876  cssval  21723  topnex  23024  islocfin  23546  hauspwpwf1  24016  itg2lcl  25782  2sqlem7  27486  scutf  27875  isismt  28560  nmcexi  32058  opabssi  32635  lsmsnorb  33384  dispcmp  33805  cnre2csqima  33857  mppspstlem  35539  colinearex  36024  itg2addnclem  37631  itg2addnc  37634  eldiophb  42713