Theorem abssi 3996

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  {cab 2741   ⊆ wss 3900

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ss 3901

This theorem is used by:  ssab2  4007  intab  4943  opabss  5175  abex  5295  relopabiALT  5811  exse2  7963  opiota  8105  mpoexw  8126  fsplitfpar  8166  tfrlem8  8430  fiprc  9110  fival  9441  hartogslem1  9573  dmttrcl  9759  rnttrcl  9760  tz9.12lem1  9831  rankuni  9916  scott0b  9974  scott0OLD  9975  r0weon  10130  alephval3  10228  aceq3lem  10238  dfac5lem4  10244  dfac2b  10248  cff  10364  cfsuc  10374  cff1  10375  cflim2  10380  cfss  10382  axdc3lem  10567  axdclem  10636  gruina  10942  nqpr  11138  infcvgaux1i  16070  4sqlem1  17170  sscpwex  18040  cssval  22043  topnex  23369  islocfin  23891  hauspwpwf1  24361  itg2lcl  26103  2sqlem7  27808  cutsf  28235  isismt  29054  nmcexi  32685  opabssi  33305  lsmsnorb  34050  dispcmp  34602  cnre2csqima  34654  mppspstlem  36544  colinearex  37040  itg2addnclem  38857  itg2addnc  38860  dfprop1  38913  eldiophb  44034