Theorem abssi 4069

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

Syntax hints:   → wi 4   ∈ wcel 2107  {cab 2713   ⊆ wss 3950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ss 3967

This theorem is referenced by:  ssab2  4078  intab  4977  opabss  5206  relopabiALT  5832  exse2  7940  opiota  8085  mpoexw  8104  fsplitfpar  8144  tfrlem8  8425  fiprc  9086  fival  9453  hartogslem1  9583  dmttrcl  9762  rnttrcl  9763  tz9.12lem1  9828  rankuni  9904  scott0  9927  r0weon  10053  alephval3  10151  aceq3lem  10161  dfac5lem4  10167  dfac5lem4OLD  10169  dfac2b  10172  cff  10289  cfsuc  10298  cff1  10299  cflim2  10304  cfss  10306  axdc3lem  10491  axdclem  10560  gruina  10859  nqpr  11055  infcvgaux1i  15894  4sqlem1  16987  sscpwex  17860  cssval  21701  topnex  23004  islocfin  23526  hauspwpwf1  23996  itg2lcl  25763  2sqlem7  27469  scutf  27858  isismt  28543  nmcexi  32046  opabssi  32626  lsmsnorb  33420  dispcmp  33859  cnre2csqima  33911  mppspstlem  35577  colinearex  36062  itg2addnclem  37679  itg2addnc  37682  eldiophb  42773