Theorem abssi 4021

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

Syntax hints:   → wi 4   ∈ wcel 2109  {cab 2707   ⊆ wss 3903

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3920

This theorem is referenced by:  ssab2  4030  intab  4928  opabss  5156  relopabiALT  5766  exse2  7850  opiota  7994  mpoexw  8013  fsplitfpar  8051  tfrlem8  8306  fiprc  8970  fival  9302  hartogslem1  9434  dmttrcl  9617  rnttrcl  9618  tz9.12lem1  9683  rankuni  9759  scott0  9782  r0weon  9906  alephval3  10004  aceq3lem  10014  dfac5lem4  10020  dfac5lem4OLD  10022  dfac2b  10025  cff  10142  cfsuc  10151  cff1  10152  cflim2  10157  cfss  10159  axdc3lem  10344  axdclem  10413  gruina  10712  nqpr  10908  infcvgaux1i  15764  4sqlem1  16860  sscpwex  17722  cssval  21589  topnex  22881  islocfin  23402  hauspwpwf1  23872  itg2lcl  25626  2sqlem7  27333  scutf  27723  isismt  28479  nmcexi  31970  opabssi  32558  lsmsnorb  33328  dispcmp  33826  cnre2csqima  33878  mppspstlem  35544  colinearex  36034  itg2addnclem  37651  itg2addnc  37654  eldiophb  42730