Theorem abssi 4020

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

Syntax hints:   → wi 4   ∈ wcel 2113  {cab 2714   ⊆ wss 3901

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3918

This theorem is referenced by:  ssab2  4031  intab  4933  opabss  5162  abex  5271  relopabiALT  5772  exse2  7859  opiota  8003  mpoexw  8022  fsplitfpar  8060  tfrlem8  8315  fiprc  8981  fival  9315  hartogslem1  9447  dmttrcl  9630  rnttrcl  9631  tz9.12lem1  9699  rankuni  9775  scott0  9798  r0weon  9922  alephval3  10020  aceq3lem  10030  dfac5lem4  10036  dfac5lem4OLD  10038  dfac2b  10041  cff  10158  cfsuc  10167  cff1  10168  cflim2  10173  cfss  10175  axdc3lem  10360  axdclem  10429  gruina  10729  nqpr  10925  infcvgaux1i  15780  4sqlem1  16876  sscpwex  17739  cssval  21637  topnex  22940  islocfin  23461  hauspwpwf1  23931  itg2lcl  25684  2sqlem7  27391  cutsf  27788  isismt  28606  nmcexi  32101  opabssi  32691  lsmsnorb  33472  dispcmp  34016  cnre2csqima  34068  mppspstlem  35765  colinearex  36254  itg2addnclem  37872  itg2addnc  37875  eldiophb  42999