Theorem abssi 4068

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

Syntax hints:   → wi 4   ∈ wcel 2107  {cab 2710   ⊆ wss 3949

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  ssab2  4077  intab  4983  opabss  5213  relopabiALT  5824  exse2  7908  opiota  8045  mpoexw  8065  fsplitfpar  8104  tfrlem8  8384  fiprc  9045  fival  9407  hartogslem1  9537  dmttrcl  9716  rnttrcl  9717  tz9.12lem1  9782  rankuni  9858  scott0  9881  r0weon  10007  alephval3  10105  aceq3lem  10115  dfac5lem4  10121  dfac2b  10125  cff  10243  cfsuc  10252  cff1  10253  cflim2  10258  cfss  10260  axdc3lem  10445  axdclem  10514  gruina  10813  nqpr  11009  infcvgaux1i  15803  4sqlem1  16881  sscpwex  17762  cssval  21235  topnex  22499  islocfin  23021  hauspwpwf1  23491  itg2lcl  25245  2sqlem7  26927  scutf  27313  isismt  27785  nmcexi  31279  opabssi  31842  lsmsnorb  32501  dispcmp  32839  cnre2csqima  32891  mppspstlem  34562  colinearex  35032  itg2addnclem  36539  itg2addnc  36542  eldiophb  41495