Theorem abssi 3969

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

Syntax hints:   → wi 4   ∈ wcel 2112  {cab 2714   ⊆ wss 3853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-in 3860  df-ss 3870

This theorem is referenced by:  ssab2  3978  intab  4875  opabss  5103  relopabiALT  5678  exse2  7673  opiota  7807  mpoexw  7827  fsplitfpar  7865  tfrlem8  8098  fiprc  8700  fival  9006  hartogslem1  9136  tz9.12lem1  9368  rankuni  9444  scott0  9467  r0weon  9591  alephval3  9689  aceq3lem  9699  dfac5lem4  9705  dfac2b  9709  cff  9827  cfsuc  9836  cff1  9837  cflim2  9842  cfss  9844  axdc3lem  10029  axdclem  10098  gruina  10397  nqpr  10593  infcvgaux1i  15384  4sqlem1  16464  sscpwex  17274  cssval  20598  topnex  21847  islocfin  22368  hauspwpwf1  22838  itg2lcl  24579  2sqlem7  26259  isismt  26579  nmcexi  30061  opabssi  30626  lsmsnorb  31247  dispcmp  31477  cnre2csqima  31529  mppspstlem  33200  scutf  33692  colinearex  34048  itg2addnclem  35514  itg2addnc  35517  eldiophb  40223