Theorem abssi 4022

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

Syntax hints:   → wi 4   ∈ wcel 2143  {cab 2741   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ss 3922

This theorem is referenced by:  ssab2  4033  intab  4943  opabss  5175  abex  5297  relopabiALT  5810  exse2  7910  opiota  8052  mpoexw  8071  fsplitfpar  8109  tfrlem8  8367  fiprc  9037  fival  9368  hartogslem1  9500  dmttrcl  9686  rnttrcl  9687  tz9.12lem1  9755  rankuni  9831  scott0  9856  r0weon  9992  alephval3  10090  aceq3lem  10100  dfac5lem4  10106  dfac2b  10110  cff  10226  cfsuc  10236  cff1  10237  cflim2  10242  cfss  10244  axdc3lem  10429  axdclem  10498  gruina  10798  nqpr  10994  infcvgaux1i  15907  4sqlem1  17003  sscpwex  17867  cssval  21832  topnex  23153  islocfin  23674  hauspwpwf1  24144  itg2lcl  25886  2sqlem7  27588  cutsf  27985  isismt  28803  nmcexi  32378  opabssi  32958  lsmsnorb  33704  dispcmp  34249  cnre2csqima  34301  mppspstlem  36063  colinearex  36552  itg2addnclem  38322  itg2addnc  38325  eldiophb  43488