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  17753  cssval  21567  topnex  22859  islocfin  23380  hauspwpwf1  23850  itg2lcl  25604  2sqlem7  27311  scutf  27700  isismt  28437  nmcexi  31928  opabssi  32514  lsmsnorb  33335  dispcmp  33822  cnre2csqima  33874  mppspstlem  35531  colinearex  36021  itg2addnclem  37638  itg2addnc  37641  eldiophb  42718