Theorem abssi 3992

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  {cab 2738   ⊆ wss 3896

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3897

This theorem is used by:  ssab2  4003  intab  4937  opabss  5168  abex  5288  relopabiALT  5802  exse2  7933  opiota  8075  mpoexw  8096  fsplitfpar  8136  tfrlem8  8400  fiprc  9080  fival  9411  hartogslem1  9543  dmttrcl  9729  rnttrcl  9730  tz9.12lem1  9801  rankuni  9886  scott0b  9944  scott0OLD  9945  r0weon  10098  alephval3  10196  aceq3lem  10206  dfac5lem4  10212  dfac2b  10216  cff  10332  cfsuc  10342  cff1  10343  cflim2  10348  cfss  10350  axdc3lem  10535  axdclem  10604  gruina  10910  nqpr  11106  infcvgaux1i  16035  4sqlem1  17135  sscpwex  17999  cssval  21997  topnex  23323  islocfin  23845  hauspwpwf1  24315  itg2lcl  26057  2sqlem7  27760  cutsf  28187  isismt  29006  nmcexi  32637  opabssi  33258  lsmsnorb  33996  dispcmp  34541  cnre2csqima  34593  mppspstlem  36454  colinearex  36949  itg2addnclem  38726  itg2addnc  38729  dfprop1  38782  eldiophb  43905