Theorem abssi 4029

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

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

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 3928

This theorem is referenced by:  ssab2  4038  intab  4938  opabss  5166  relopabiALT  5777  exse2  7873  opiota  8017  mpoexw  8036  fsplitfpar  8074  tfrlem8  8329  fiprc  8993  fival  9339  hartogslem1  9471  dmttrcl  9650  rnttrcl  9651  tz9.12lem1  9716  rankuni  9792  scott0  9815  r0weon  9941  alephval3  10039  aceq3lem  10049  dfac5lem4  10055  dfac5lem4OLD  10057  dfac2b  10060  cff  10177  cfsuc  10186  cff1  10187  cflim2  10192  cfss  10194  axdc3lem  10379  axdclem  10448  gruina  10747  nqpr  10943  infcvgaux1i  15799  4sqlem1  16895  sscpwex  17757  cssval  21624  topnex  22916  islocfin  23437  hauspwpwf1  23907  itg2lcl  25661  2sqlem7  27368  scutf  27758  isismt  28514  nmcexi  32005  opabssi  32591  lsmsnorb  33355  dispcmp  33842  cnre2csqima  33894  mppspstlem  35551  colinearex  36041  itg2addnclem  37658  itg2addnc  37661  eldiophb  42738