Theorem abssi 3710

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

Syntax hints:   → wi 4   ∈ wcel 2030  {cab 2637   ⊆ wss 3607

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-in 3614  df-ss 3621

This theorem is referenced by:  ssab2  3719  intab  4539  opabss  4747  relopabiALT  5279  exse2  7147  opiota  7273  tfrlem8  7525  fiprc  8080  fival  8359  hartogslem1  8488  tz9.12lem1  8688  rankuni  8764  scott0  8787  r0weon  8873  alephval3  8971  aceq3lem  8981  dfac5lem4  8987  dfac2  8991  cff  9108  cfsuc  9117  cff1  9118  cflim2  9123  cfss  9125  axdc3lem  9310  axdclem  9379  gruina  9678  nqpr  9874  infcvgaux1i  14633  4sqlem1  15699  sscpwex  16522  symgval  17845  cssval  20074  topnex  20848  islocfin  21368  hauspwpwf1  21838  itg2lcl  23539  2sqlem7  25194  isismt  25474  nmcexi  29013  opabssi  29551  dispcmp  30054  cnre2csqima  30085  mppspstlem  31594  scutf  32044  colinearex  32292  itg2addnclem  33591  itg2addnc  33594  eldiophb  37637