Theorem abssi 3930

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

Syntax hints:   → wi 4   ∈ wcel 2050  {cab 2752   ⊆ wss 3823

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2744

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-in 3830  df-ss 3837

This theorem is referenced by:  ssab2  3939  intab  4773  opabss  4987  relopabiALT  5539  exse2  7431  opiota  7559  mpoexw  7578  tfrlem8  7818  fiprc  8386  fival  8665  hartogslem1  8795  tz9.12lem1  9004  rankuni  9080  scott0  9103  r0weon  9226  alephval3  9324  aceq3lem  9334  dfac5lem4  9340  dfac2b  9344  cff  9462  cfsuc  9471  cff1  9472  cflim2  9477  cfss  9479  axdc3lem  9664  axdclem  9733  gruina  10032  nqpr  10228  infcvgaux1i  15066  4sqlem1  16134  sscpwex  16937  symgval  18262  cssval  20522  topnex  21302  islocfin  21823  hauspwpwf1  22293  itg2lcl  24025  2sqlem7  25696  isismt  26016  nmcexi  29578  opabssi  30122  dispcmp  30767  cnre2csqima  30798  mppspstlem  32338  scutf  32794  colinearex  33042  itg2addnclem  34384  itg2addnc  34387  eldiophb  38749