Theorem abssi 3999

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

Syntax hints:   → wi 4   ∈ wcel 2119  {cab 2717   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ss 3900

This theorem is referenced by:  ssab2  4010  intab  4908  opabss  5136  abex  5254  relopabiALT  5766  exse2  7857  opiota  8001  mpoexw  8020  fsplitfpar  8057  tfrlem8  8313  fiprc  8981  fival  9315  hartogslem1  9447  dmttrcl  9633  rnttrcl  9634  tz9.12lem1  9702  rankuni  9778  scott0  9801  r0weon  9925  alephval3  10023  aceq3lem  10033  dfac5lem4  10039  dfac5lem4OLD  10041  dfac2b  10044  cff  10161  cfsuc  10170  cff1  10171  cflim2  10176  cfss  10178  axdc3lem  10363  axdclem  10432  gruina  10732  nqpr  10928  infcvgaux1i  15813  4sqlem1  16910  sscpwex  17773  cssval  21657  topnex  22979  islocfin  23500  hauspwpwf1  23970  itg2lcl  25712  2sqlem7  27405  cutsf  27802  isismt  28620  nmcexi  32115  opabssi  32705  lsmsnorb  33474  dispcmp  34043  cnre2csqima  34095  mppspstlem  35799  colinearex  36288  itg2addnclem  38038  itg2addnc  38041  eldiophb  43206