Theorem abssi 4045

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

Syntax hints:   → wi 4   ∈ wcel 2110  {cab 2799   ⊆ wss 3935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-in 3942  df-ss 3951

This theorem is referenced by:  ssab2  4054  intab  4905  opabss  5129  relopabiALT  5694  exse2  7621  opiota  7756  mpoexw  7775  fsplitfpar  7813  tfrlem8  8019  fiprc  8594  fival  8875  hartogslem1  9005  tz9.12lem1  9215  rankuni  9291  scott0  9314  r0weon  9437  alephval3  9535  aceq3lem  9545  dfac5lem4  9551  dfac2b  9555  cff  9669  cfsuc  9678  cff1  9679  cflim2  9684  cfss  9686  axdc3lem  9871  axdclem  9940  gruina  10239  nqpr  10435  infcvgaux1i  15211  4sqlem1  16283  sscpwex  17084  cssval  20825  topnex  21603  islocfin  22124  hauspwpwf1  22594  itg2lcl  24327  2sqlem7  25999  isismt  26319  nmcexi  29802  opabssi  30363  lsmsnorb  30945  dispcmp  31123  cnre2csqima  31154  mppspstlem  32818  scutf  33273  colinearex  33521  itg2addnclem  34942  itg2addnc  34945  eldiophb  39352