Theorem abssi 4035

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

Syntax hints:   → wi 4   ∈ wcel 2109  {cab 2708   ⊆ wss 3916

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ss 3933

This theorem is referenced by:  ssab2  4044  intab  4944  opabss  5173  relopabiALT  5788  exse2  7895  opiota  8040  mpoexw  8059  fsplitfpar  8099  tfrlem8  8354  fiprc  9018  fival  9369  hartogslem1  9501  dmttrcl  9680  rnttrcl  9681  tz9.12lem1  9746  rankuni  9822  scott0  9845  r0weon  9971  alephval3  10069  aceq3lem  10079  dfac5lem4  10085  dfac5lem4OLD  10087  dfac2b  10090  cff  10207  cfsuc  10216  cff1  10217  cflim2  10222  cfss  10224  axdc3lem  10409  axdclem  10478  gruina  10777  nqpr  10973  infcvgaux1i  15829  4sqlem1  16925  sscpwex  17783  cssval  21597  topnex  22889  islocfin  23410  hauspwpwf1  23880  itg2lcl  25634  2sqlem7  27341  scutf  27730  isismt  28467  nmcexi  31961  opabssi  32547  lsmsnorb  33368  dispcmp  33855  cnre2csqima  33907  mppspstlem  35558  colinearex  36043  itg2addnclem  37660  itg2addnc  37663  eldiophb  42738