Theorem abssi 4050

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

Syntax hints:   → wi 4   ∈ wcel 2109  {cab 2714   ⊆ wss 3931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ss 3948

This theorem is referenced by:  ssab2  4059  intab  4959  opabss  5188  relopabiALT  5807  exse2  7918  opiota  8063  mpoexw  8082  fsplitfpar  8122  tfrlem8  8403  fiprc  9064  fival  9429  hartogslem1  9561  dmttrcl  9740  rnttrcl  9741  tz9.12lem1  9806  rankuni  9882  scott0  9905  r0weon  10031  alephval3  10129  aceq3lem  10139  dfac5lem4  10145  dfac5lem4OLD  10147  dfac2b  10150  cff  10267  cfsuc  10276  cff1  10277  cflim2  10282  cfss  10284  axdc3lem  10469  axdclem  10538  gruina  10837  nqpr  11033  infcvgaux1i  15878  4sqlem1  16973  sscpwex  17833  cssval  21647  topnex  22939  islocfin  23460  hauspwpwf1  23930  itg2lcl  25685  2sqlem7  27392  scutf  27781  isismt  28518  nmcexi  32012  opabssi  32598  lsmsnorb  33411  dispcmp  33895  cnre2csqima  33947  mppspstlem  35598  colinearex  36083  itg2addnclem  37700  itg2addnc  37703  eldiophb  42755