Theorem abssi 3640

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

Syntax hints:   → wi 4   ∈ wcel 1977  {cab 2596   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-in 3547  df-ss 3554

This theorem is referenced by:  ssab2  3649  intab  4442  opabss  4646  relopabiALT  5168  exse2  6998  opiota  7118  tfrlem8  7367  fiprc  7924  fival  8201  hartogslem1  8330  tz9.12lem1  8533  rankuni  8609  scott0  8632  r0weon  8718  alephval3  8816  aceq3lem  8826  dfac5lem4  8832  dfac2  8836  cff  8953  cfsuc  8962  cff1  8963  cflim2  8968  cfss  8970  axdc3lem  9155  axdclem  9224  gruina  9519  nqpr  9715  infcvgaux1i  14428  4sqlem1  15490  sscpwex  16298  symgval  17622  cssval  19845  islocfin  21130  hauspwpwf1  21601  itg2lcl  23300  2sqlem7  24949  isismt  25229  nmcexi  28269  dispcmp  29254  cnre2csqima  29285  mppspstlem  30722  colinearex  31337  bj-topnex  32247  itg2addnclem  32631  itg2addnc  32634  eldiophb  36338