Theorem abssi 4016

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  {cab 2739   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ss 3916

This theorem is used by:  ssab2  4027  intab  4938  opabss  5169  abex  5288  relopabiALT  5801  exse2  7929  opiota  8070  mpoexw  8091  fsplitfpar  8129  tfrlem8  8392  fiprc  9072  fival  9404  hartogslem1  9536  dmttrcl  9722  rnttrcl  9723  tz9.12lem1  9794  rankuni  9879  scott0b  9937  scott0OLD  9938  r0weon  10091  alephval3  10189  aceq3lem  10199  dfac5lem4  10205  dfac2b  10209  cff  10325  cfsuc  10335  cff1  10336  cflim2  10341  cfss  10343  axdc3lem  10528  axdclem  10597  gruina  10903  nqpr  11099  infcvgaux1i  16026  4sqlem1  17126  sscpwex  17990  cssval  21988  topnex  23314  islocfin  23836  hauspwpwf1  24306  itg2lcl  26048  2sqlem7  27751  cutsf  28178  isismt  28997  nmcexi  32628  opabssi  33207  lsmsnorb  33946  dispcmp  34491  cnre2csqima  34543  mppspstlem  36336  colinearex  36825  itg2addnclem  38589  itg2addnc  38592  dfprop1  38645  eldiophb  43767