Theorem abssi 4003

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

Syntax hints:   → wi 4   ∈ wcel 2106  {cab 2715   ⊆ wss 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904

This theorem is referenced by:  ssab2  4012  intab  4909  opabss  5138  relopabiALT  5733  exse2  7764  opiota  7899  mpoexw  7919  fsplitfpar  7959  tfrlem8  8215  fiprc  8835  fival  9171  hartogslem1  9301  dmttrcl  9479  rnttrcl  9480  tz9.12lem1  9545  rankuni  9621  scott0  9644  r0weon  9768  alephval3  9866  aceq3lem  9876  dfac5lem4  9882  dfac2b  9886  cff  10004  cfsuc  10013  cff1  10014  cflim2  10019  cfss  10021  axdc3lem  10206  axdclem  10275  gruina  10574  nqpr  10770  infcvgaux1i  15569  4sqlem1  16649  sscpwex  17527  cssval  20887  topnex  22146  islocfin  22668  hauspwpwf1  23138  itg2lcl  24892  2sqlem7  26572  isismt  26895  nmcexi  30388  opabssi  30953  lsmsnorb  31579  dispcmp  31809  cnre2csqima  31861  mppspstlem  33533  scutf  34006  colinearex  34362  itg2addnclem  35828  itg2addnc  35831  eldiophb  40579