Theorem abssi 3999

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

Syntax hints:   → wi 4   ∈ wcel 2108  {cab 2715   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  ssab2  4008  intab  4906  opabss  5134  relopabiALT  5722  exse2  7738  opiota  7872  mpoexw  7892  fsplitfpar  7930  tfrlem8  8186  fiprc  8789  fival  9101  hartogslem1  9231  tz9.12lem1  9476  rankuni  9552  scott0  9575  r0weon  9699  alephval3  9797  aceq3lem  9807  dfac5lem4  9813  dfac2b  9817  cff  9935  cfsuc  9944  cff1  9945  cflim2  9950  cfss  9952  axdc3lem  10137  axdclem  10206  gruina  10505  nqpr  10701  infcvgaux1i  15497  4sqlem1  16577  sscpwex  17444  cssval  20799  topnex  22054  islocfin  22576  hauspwpwf1  23046  itg2lcl  24797  2sqlem7  26477  isismt  26799  nmcexi  30289  opabssi  30854  lsmsnorb  31481  dispcmp  31711  cnre2csqima  31763  mppspstlem  33433  dmttrcl  33707  rnttrcl  33708  scutf  33933  colinearex  34289  itg2addnclem  35755  itg2addnc  35758  eldiophb  40495