Theorem abssi 4008

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

Syntax hints:   → wi 4   ∈ wcel 2114  {cab 2714   ⊆ wss 3889

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3906

This theorem is referenced by:  ssab2  4019  intab  4920  opabss  5149  abex  5267  relopabiALT  5779  exse2  7868  opiota  8012  mpoexw  8031  fsplitfpar  8068  tfrlem8  8323  fiprc  8991  fival  9325  hartogslem1  9457  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  15822  4sqlem1  16919  sscpwex  17782  cssval  21662  topnex  22961  islocfin  23482  hauspwpwf1  23952  itg2lcl  25694  2sqlem7  27387  cutsf  27784  isismt  28602  nmcexi  32097  opabssi  32686  lsmsnorb  33451  dispcmp  34003  cnre2csqima  34055  mppspstlem  35753  colinearex  36242  itg2addnclem  37992  itg2addnc  37995  eldiophb  43189