Theorem abssi 4048

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

Syntax hints:   → wi 4   ∈ wcel 2114  {cab 2801   ⊆ wss 3938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-in 3945  df-ss 3954

This theorem is referenced by:  ssab2  4057  intab  4908  opabss  5132  relopabiALT  5697  exse2  7624  opiota  7759  mpoexw  7778  fsplitfpar  7816  tfrlem8  8022  fiprc  8597  fival  8878  hartogslem1  9008  tz9.12lem1  9218  rankuni  9294  scott0  9317  r0weon  9440  alephval3  9538  aceq3lem  9548  dfac5lem4  9554  dfac2b  9558  cff  9672  cfsuc  9681  cff1  9682  cflim2  9687  cfss  9689  axdc3lem  9874  axdclem  9943  gruina  10242  nqpr  10438  infcvgaux1i  15214  4sqlem1  16286  sscpwex  17087  cssval  20828  topnex  21606  islocfin  22127  hauspwpwf1  22597  itg2lcl  24330  2sqlem7  26002  isismt  26322  nmcexi  29805  opabssi  30366  lsmsnorb  30947  dispcmp  31125  cnre2csqima  31156  mppspstlem  32820  scutf  33275  colinearex  33523  itg2addnclem  34945  itg2addnc  34948  eldiophb  39361