Theorem abssi 4018

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

Syntax hints:   → wi 4   ∈ wcel 2113  {cab 2712   ⊆ wss 3899

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 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ss 3916

This theorem is referenced by:  ssab2  4029  intab  4931  opabss  5160  abex  5269  relopabiALT  5770  exse2  7857  opiota  8001  mpoexw  8020  fsplitfpar  8058  tfrlem8  8313  fiprc  8979  fival  9313  hartogslem1  9445  dmttrcl  9628  rnttrcl  9629  tz9.12lem1  9697  rankuni  9773  scott0  9796  r0weon  9920  alephval3  10018  aceq3lem  10028  dfac5lem4  10034  dfac5lem4OLD  10036  dfac2b  10039  cff  10156  cfsuc  10165  cff1  10166  cflim2  10171  cfss  10173  axdc3lem  10358  axdclem  10427  gruina  10727  nqpr  10923  infcvgaux1i  15778  4sqlem1  16874  sscpwex  17737  cssval  21635  topnex  22938  islocfin  23459  hauspwpwf1  23929  itg2lcl  25682  2sqlem7  27389  scutf  27780  isismt  28555  nmcexi  32050  opabssi  32640  lsmsnorb  33421  dispcmp  33965  cnre2csqima  34017  mppspstlem  35714  colinearex  36203  itg2addnclem  37811  itg2addnc  37814  eldiophb  42941