Theorem abssi 4022

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

Syntax hints:   → wi 4   ∈ wcel 2114  {cab 2715   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3920

This theorem is referenced by:  ssab2  4033  intab  4935  opabss  5164  abex  5273  relopabiALT  5780  exse2  7869  opiota  8013  mpoexw  8032  fsplitfpar  8070  tfrlem8  8325  fiprc  8993  fival  9327  hartogslem1  9459  dmttrcl  9642  rnttrcl  9643  tz9.12lem1  9711  rankuni  9787  scott0  9810  r0weon  9934  alephval3  10032  aceq3lem  10042  dfac5lem4  10048  dfac5lem4OLD  10050  dfac2b  10053  cff  10170  cfsuc  10179  cff1  10180  cflim2  10185  cfss  10187  axdc3lem  10372  axdclem  10441  gruina  10741  nqpr  10937  infcvgaux1i  15792  4sqlem1  16888  sscpwex  17751  cssval  21649  topnex  22952  islocfin  23473  hauspwpwf1  23943  itg2lcl  25696  2sqlem7  27403  cutsf  27800  isismt  28618  nmcexi  32114  opabssi  32703  lsmsnorb  33484  dispcmp  34037  cnre2csqima  34089  mppspstlem  35787  colinearex  36276  itg2addnclem  37922  itg2addnc  37925  eldiophb  43114